1 /-
2 Copyright (c) 2017 Johannes Hölzl. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Johannes Hölzl, Mario Carneiro, Jeremy Avigad
5 -/
6
7 import order.filter
src └──────────┘
8
9 /-!
10 # Basic theory of topological spaces.
11
12 The main definition is the type class `topological space α` which endows a type `α` with a topology.
13 Then `set α` gets predicates `is_open`, `is_closed` and functions `interior`, `closure` and
14 `frontier`. Each point `x` of `α` gets a neighborhood filter `𝓝 x`.
15
16 This file also defines locally finite families of subsets of `α`.
17
18 For topological spaces `α` and `β`, a function `f : α → β` and a point `a : α`,
19 `continuous_at f a` means `f` is continuous at `a`, and global continuity is
20 `continuous f`. There is also a version of continuity `pcontinuous` for
21 partially defined functions.
22
23 ## Implementation notes
24
25 Topology in mathlib heavily uses filters (even more than in Bourbaki). See explanations in
26 `docs/theories/topology.md`.
27
28 ## References
29
30 * [N. Bourbaki, *General Topology*][bourbaki1966]
31 * [I. M. James, *Topologies and Uniformities*][james1999]
32
33 ## Tags
34
35 topological space, interior, closure, frontier, neighborhood, continuity, continuous function
36 -/
37
38 open set filter lattice classical
39 open_locale classical
40
41 universes u v w
42
43 /-- A topology on `α`. -/
44 structure topological_space (α : Type u) :=
id └──┘
typ └──┘
45 (is_open : set α → Prop)
id └─┘ ┴ ┴
src └─┘
typ └─┘ ┴ ┴
46 (is_open_univ : is_open univ)
id └─────┘ └──┘
src └──┘
typ └─────┘ └──┘
47 (is_open_inter : ∀s t, is_open s → is_open t → is_open (s ∩ t))
id ┴ ┴ └─────┘ ┴ └─────┘ ┴ └─────┘ ┴ ┴ ┴
src ┴
typ ┴ ┴ └─────┘ ┴ └─────┘ ┴ └─────┘ ┴ ┴ ┴
48 (is_open_sUnion : ∀s, (∀t∈s, is_open t) → is_open (⋃₀ s))
id ┴ ┴ ┴ └─────┘ ┴ └─────┘ └┘ ┴
src ┴ └┘
typ ┴ ┴ ┴ └─────┘ ┴ └─────┘ └┘ ┴
49
50 attribute [class] topological_space
id └───────────────┘
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
51
52 section topological_space
53
54 variables {α : Type u} {β : Type v} {ι : Sort w} {a : α} {s s₁ s₂ : set α} {p p₁ p₂ : α → Prop}
id ┴ └─┘
src └─┘
typ ┴ └─┘
55
56 @[ext]
doc └─┘
57 lemma topological_space_eq : ∀ {f g : topological_space α}, f.is_open = g.is_open → f = g
id ┴ └───────────────┘ ┴ ┴└──────┘ ┴ ┴└──────┘ ┴ ┴ ┴
src └───────────────┘ └──────┘ ┴ └──────┘ ┴
typ ┴ └───────────────┘ ┴ ┴└──────┘ ┴ ┴└──────┘ ┴ ┴ ┴
doc └───────────────┘
58 | ⟨a, _, _, _⟩ ⟨b, _, _, _⟩ rfl := rfl
id └─┘ └─┘
src └─┘ └─┘
typ └─┘ └─┘
59
60 section
61 variables [t : topological_space α]
id └───────────────┘
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
62 include t
63
64 /-- `is_open s` means that `s` is open in the ambient topological space on `α` -/
65 def is_open (s : set α) : Prop := topological_space.is_open t s
id └─┘ ┴ └───────────────────────┘ ┴ ┴
src └─┘ └───────────────────────┘
typ └─┘ ┴ └───────────────────────┘ ┴ ┴
66
67 @[simp]
doc └──┘
68 lemma is_open_univ : is_open (univ : set α) := topological_space.is_open_univ t
id └─────┘ └──┘ └─┘ ┴ └────────────────────────────┘ ┴
src └─────┘ └──┘ └─┘ └────────────────────────────┘
typ └─────┘ └──┘ └─┘ ┴ └────────────────────────────┘ ┴
doc └─────┘
69
70 lemma is_open_inter (h₁ : is_open s₁) (h₂ : is_open s₂) : is_open (s₁ ∩ s₂) :=
id └─────┘ └┘ └─────┘ └┘ └─────┘ └┘ ┴ └┘
src └─────┘ └─────┘ └─────┘ ┴
typ └─────┘ └┘ └─────┘ └┘ └─────┘ └┘ ┴ └┘
doc └─────┘ └─────┘ └─────┘
71 topological_space.is_open_inter t s₁ s₂ h₁ h₂
id └─────────────────────────────┘ ┴ └┘ └┘ └┘ └┘
src └─────────────────────────────┘
typ └─────────────────────────────┘ ┴ └┘ └┘ └┘ └┘
72
73 lemma is_open_sUnion {s : set (set α)} (h : ∀t ∈ s, is_open t) : is_open (⋃₀ s) :=
id └─┘ └─┘ ┴ ┴ ┴ └─────┘ ┴ └─────┘ └┘ ┴
src └─┘ └─┘ └─────┘ └─────┘ └┘
typ └─┘ └─┘ ┴ ┴ ┴ └─────┘ ┴ └─────┘ └┘ ┴
doc └─────┘ └─────┘
74 topological_space.is_open_sUnion t s h
id └──────────────────────────────┘ ┴ ┴ ┴
src └──────────────────────────────┘
typ └──────────────────────────────┘ ┴ ┴ ┴
75
76 end
77
78 lemma is_open_fold {s : set α} {t : topological_space α} : t.is_open s = @is_open α t s :=
id └─┘ ┴ └───────────────┘ ┴ ┴└──────┘ ┴ ┴ └─────┘ ┴ ┴ ┴
src └─┘ └───────────────┘ └──────┘ ┴ └─────┘
typ └─┘ ┴ └───────────────┘ ┴ ┴└──────┘ ┴ ┴ └─────┘ ┴ ┴ ┴
doc └───────────────┘ └─────┘
79 rfl
id └─┘
src └─┘
typ └─┘
80
81 variables [topological_space α]
id └───────────────┘
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
82
83 lemma is_open_Union {f : ι → set α} (h : ∀i, is_open (f i)) : is_open (⋃i, f i) :=
id ┴ └─┘ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴┴┴ ┴ ┴
src └─┘ └─────┘ └─────┘ ┴ ┴
typ ┴ └─┘ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴┴┴ ┴ ┴
doc └─────┘ └─────┘ ┴ ┴
84 is_open_sUnion $ by rintro _ ⟨i, rfl⟩; exact h i
id └────────────┘ ┴ ┴
src └────────────┘ └───────────────┘ └────┘ ┴ └
typ └────────────┘ └───────────────┘ └────┘┴┴┴└
doc └───────────────┘ └────┘ ┴ └
txt └───────────────┘ └────┘ ┴ └
par └───────────────┘ └────┘ ┴ └
pid └─────────┘ ┴ ┴ └
st └─────────────────────────────
85
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
86 lemma is_open_bUnion {s : set β} {f : β → set α} (h : ∀i∈s, is_open (f i)) :
id └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ └─────┘ ┴ ┴
src └─┘ └─┘ └─────┘
typ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ └─────┘ ┴ ┴
doc └─────┘
87 is_open (⋃i∈s, f i) :=
id └─────┘ ┴┴ ┴┴ ┴ ┴
src └─────┘ ┴ ┴
typ └─────┘ ┴┴ ┴┴ ┴ ┴
doc └─────┘ ┴ ┴
88 is_open_Union $ assume i, is_open_Union $ assume hi, h i hi
id └───────────┘ ┴ └───────────┘ └┘ ┴ ┴ └┘
src └───────────┘ └───────────┘
typ └───────────┘ ┴ └───────────┘ └┘ ┴ ┴ └┘
89
90 lemma is_open_union (h₁ : is_open s₁) (h₂ : is_open s₂) : is_open (s₁ ∪ s₂) :=
id └─────┘ └┘ └─────┘ └┘ └─────┘ └┘ ┴ └┘
src └─────┘ └─────┘ └─────┘ ┴
typ └─────┘ └┘ └─────┘ └┘ └─────┘ └┘ ┴ └┘
doc └─────┘ └─────┘ └─────┘
91 by rw union_eq_Union; exact is_open_Union (bool.forall_bool.2 ⟨h₂, h₁⟩)
id └────────────┘ └───────────┘ └──────────────┘ └┘ └┘
src └─┘└────────────┘ └────┘└───────────┘┴ └──────────────┘└─┘ └┘ └──
typ └─┘└────────────┘ └────┘└───────────┘┴ └──────────────┘└─┘ └┘└┘└┘└──
doc └─┘ └────┘ ┴ └─┘ └┘ └──
txt └─┘ └────┘ ┴ └─┘ └┘ └──
par └─┘ └────┘ ┴ └─┘ └┘ └──
pid ┴ ┴ ┴ └─┘ └┘ └┘└
st └─────────────────────────────────────────────────────────────────────
92
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
93 @[simp] lemma is_open_empty : is_open (∅ : set α) :=
id └─────┘ ┴ └─┘ ┴
src └─────┘ ┴ └─┘
typ └─────┘ ┴ └─┘ ┴
doc └──┘ └─────┘
94 by rw ← sUnion_empty; exact is_open_sUnion (assume a, false.elim)
id └──────────┘ └────────────┘ └────────┘
src └───┘└──────────┘ └────┘└────────────┘┴ └──┘└────────┘└─
typ └───┘└──────────┘ └────┘└────────────┘┴ └──┘└────────┘└─
doc └───┘ └────┘ ┴ └──┘ └─
txt └───┘ └────┘ ┴ └──┘ └─
par └───┘ └────┘ ┴ └──┘ └─
pid └─┘ ┴ ┴ └──┘ ┴└
st └───────────────────────────────────────────────────────────────
95
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
96 lemma is_open_sInter {s : set (set α)} (hs : finite s) : (∀t ∈ s, is_open t) → is_open (⋂₀ s) :=
id └─┘ └─┘ ┴ └────┘ ┴ ┴ ┴ └─────┘ ┴ └─────┘ └┘ ┴
src └─┘ └─┘ └────┘ └─────┘ └─────┘ └┘
typ └─┘ └─┘ ┴ └────┘ ┴ ┴ ┴ └─────┘ ┴ └─────┘ └┘ ┴
doc └────┘ └─────┘ └─────┘ └┘
97 finite.induction_on hs (λ _, by rw sInter_empty; exact is_open_univ) $
id └─────────────────┘ └┘ ┴ └──────────┘ └──────────┘
src └─────────────────┘ └─┘└──────────┘ └────┘└──────────┘
typ └─────────────────┘ └┘ ┴ └─┘└──────────┘ └────┘└──────────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ ┴
st └──────────────────────────────────┘
98 λ a s has hs ih h, by rw sInter_insert; exact
id ┴ ┴ └─┘ └┘ └┘ ┴ └───────────┘
src └─┘└───────────┘ └────┘
typ ┴ ┴ └─┘ └┘ └┘ ┴ └─┘└───────────┘ └────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ ┴
st └────────────────────────
99 is_open_inter (h _ $ mem_insert _ _) (ih $ λ t, h t ∘ mem_insert_of_mem _)
id └───────────┘ └────────┘ └┘ ┴ ┴ └───────────────┘
src └───────────┘┴ └─┘ ┴└────────┘└────┘ ┴ ┴ └──┘ ┴ ┴┴┴└───────────────┘└───
typ └───────────┘┴ └─┘ ┴└────────┘└────┘ └┘┴ ┴ └──┘┴┴ ┴┴┴└───────────────┘└───
doc ┴ └─┘ ┴ └────┘ ┴ ┴ └──┘ ┴ ┴ ┴ └───
txt ┴ └─┘ ┴ └────┘ ┴ ┴ └──┘ ┴ ┴ ┴ └───
par ┴ └─┘ ┴ └────┘ ┴ ┴ └──┘ ┴ ┴ ┴ └───
pid ┴ └─┘ ┴ └────┘ ┴ ┴ └──┘ ┴ ┴ ┴ └─┘└
st ───────────────────────────────────────────────────────────────────────────
100
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
101 lemma is_open_bInter {s : set β} {f : β → set α} (hs : finite s) :
id └─┘ ┴ ┴ └─┘ ┴ └────┘ ┴
src └─┘ └─┘ └────┘
typ └─┘ ┴ ┴ └─┘ ┴ └────┘ ┴
doc └────┘
102 (∀i∈s, is_open (f i)) → is_open (⋂i∈s, f i) :=
id ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴┴ ┴┴ ┴ ┴
src └─────┘ └─────┘ ┴ ┴
typ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴┴ ┴┴ ┴ ┴
doc └─────┘ └─────┘ ┴ ┴
103 finite.induction_on hs
id └─────────────────┘ └┘
src └─────────────────┘
typ └─────────────────┘ └┘
104 (λ _, by rw bInter_empty; exact is_open_univ)
id ┴ └──────────┘ └──────────┘
src └─┘└──────────┘ └────┘└──────────┘
typ ┴ └─┘└──────────┘ └────┘└──────────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ ┴
st └──────────────────────────────────┘
105 (λ a s has hs ih h, by rw bInter_insert; exact
id ┴ ┴ └─┘ └┘ └┘ ┴ └───────────┘
src └─┘└───────────┘ └─────
typ ┴ ┴ └─┘ └┘ └┘ ┴ └─┘└───────────┘ └─────
doc └─┘ └─────
txt └─┘ └─────
par └─┘ └─────
pid ┴ └
st ┴ └────────────────────────
106 is_open_inter (h a (mem_insert _ _)) (ih (λ i hi, h i (mem_insert_of_mem _ hi))))
id └───────────┘ ┴ └────────┘ └┘ ┴ └───────────────┘
src ───┘└───────────┘┴ ┴ ┴ └────────┘└─────┘ ┴ └─────┘ ┴ ┴ └───────────────┘└─┘ └─┘
typ ───┘└───────────┘┴ ┴┴┴ └────────┘└─────┘ └┘┴ └─────┘┴┴ ┴ └───────────────┘└─┘ └─┘
doc ───┘ ┴ ┴ ┴ └─────┘ ┴ └─────┘ ┴ ┴ └─┘ └─┘
txt ───┘ ┴ ┴ ┴ └─────┘ ┴ └─────┘ ┴ ┴ └─┘ └─┘
par ───┘ ┴ ┴ ┴ └─────┘ ┴ └─────┘ ┴ ┴ └─┘ └─┘
pid ───┘ ┴ ┴ ┴ └─────┘ ┴ └─────┘ ┴ ┴ └─┘ └─┘
st ───────────────────────────────────────────────────────────────────────────────────┘
107
108 lemma is_open_Inter [fintype β] {s : β → set α}
id └─────┘ ┴ ┴ └─┘ ┴
src └─────┘ └─┘
typ └─────┘ ┴ ┴ └─┘ ┴
doc └─────┘
109 (h : ∀ i, is_open (s i)) : is_open (⋂ i, s i) :=
id ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴┴ ┴ ┴
src └─────┘ └─────┘ ┴ ┴
typ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴┴ ┴ ┴
doc └─────┘ └─────┘ ┴ ┴
110 suffices is_open (⋂ (i : β) (hi : i ∈ @univ β), s i), by simpa,
id └─────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ └──┘ ┴ └───┘
typ └─────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ └───┘
doc └─────┘ ┴ ┴ └───┘
txt └───┘
par └───┘
st └────┘
111 is_open_bInter finite_univ (λ i _, h i)
id └────────────┘ └─────────┘ ┴ ┴ ┴ ┴
src └────────────┘ └─────────┘
typ └────────────┘ └─────────┘ ┴ ┴ ┴ ┴
112
113 lemma is_open_Inter_prop {p : Prop} {s : p → set α}
id ┴ └─┘ ┴
src └─┘
typ ┴ └─┘ ┴
114 (h : ∀ h : p, is_open (s h)) : is_open (Inter s) :=
id ┴ └─────┘ ┴ ┴ └─────┘ └───┘ ┴
src └─────┘ └─────┘ └───┘
typ ┴ └─────┘ ┴ ┴ └─────┘ └───┘ ┴
doc └─────┘ └─────┘ └───┘
115 by by_cases p; simp *
id ┴
src └───────┘ └──────
typ └───────┘┴ └──────
doc └───────┘ └──────
txt └───────┘ └──────
par └───────┘ └──────
pid ┴ ┴┴└
st └───────────────────
116
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
117 lemma is_open_const {p : Prop} : is_open {a : α | p} :=
id └─────┘ ┴ ┴ ┴
src └─────┘ ┴
typ └─────┘ ┴ ┴ ┴
doc └─────┘
118 by_cases
id └──────┘
src └──────┘
typ └──────┘
119 (assume : p, begin simp only [this]; exact is_open_univ end)
id ┴ └──┘ └──────────┘
src └─────────┘ ┴ └────┘└──────────┘┴
typ ┴ └─────────┘└──┘┴ └────┘└──────────┘┴
doc └─────────┘ ┴ └────┘ ┴
txt └─────────┘ ┴ └────┘ ┴
par └─────────┘ ┴ └────┘ ┴
pid ┴└──┘└┘ ┴ ┴ ┴
st └─────────────────────────────────────────┘└─┘
120 (assume : ¬ p, begin simp only [this]; exact is_open_empty end)
id ┴ ┴ └──┘ └───────────┘
src ┴ └─────────┘ ┴ └────┘└───────────┘┴
typ ┴ ┴ └─────────┘└──┘┴ └────┘└───────────┘┴
doc └─────────┘ ┴ └────┘ ┴
txt └─────────┘ ┴ └────┘ ┴
par └─────────┘ ┴ └────┘ ┴
pid ┴└──┘└┘ ┴ ┴ ┴
st └──────────────────────────────────────────┘└─┘
121
122 lemma is_open_and : is_open {a | p₁ a} → is_open {a | p₂ a} → is_open {a | p₁ a ∧ p₂ a} :=
id └─────┘ ┴┴ └┘ ┴ └─────┘ ┴┴ └┘ ┴ └─────┘ ┴┴ └┘ ┴ ┴ └┘ ┴
src └─────┘ ┴ └─────┘ ┴ └─────┘ ┴ ┴
typ └─────┘ ┴┴ └┘ ┴ └─────┘ ┴┴ └┘ ┴ └─────┘ ┴┴ └┘ ┴ ┴ └┘ ┴
doc └─────┘ └─────┘ └─────┘
123 is_open_inter
id └───────────┘
src └───────────┘
typ └───────────┘
124
125 /-- A set is closed if its complement is open -/
126 def is_closed (s : set α) : Prop := is_open (-s)
id └─┘ ┴ └─────┘ ┴┴
src └─┘ └─────┘ ┴
typ └─┘ ┴ └─────┘ ┴┴
doc └─────┘
127
128 @[simp] lemma is_closed_empty : is_closed (∅ : set α) :=
id └───────┘ ┴ └─┘ ┴
src └───────┘ ┴ └─┘
typ └───────┘ ┴ └─┘ ┴
doc └──┘ └───────┘
129 by unfold is_closed; rw compl_empty; exact is_open_univ
id └─────────┘ └──────────┘
src └──────────────┘ └─┘└─────────┘ └────┘└──────────┘└
typ └──────────────┘ └─┘└─────────┘ └────┘└──────────┘└
doc └──────────────┘ └─┘ └────┘ └
txt └──────────────┘ └─┘ └────┘ └
par └──────────────┘ └─┘ └────┘ └
pid └────────┘ ┴ ┴ └
st └────────────────────┘└─────────┘└────────────────────
130
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
131 @[simp] lemma is_closed_univ : is_closed (univ : set α) :=
id └───────┘ └──┘ └─┘ ┴
src └───────┘ └──┘ └─┘
typ └───────┘ └──┘ └─┘ ┴
doc └──┘ └───────┘
132 by unfold is_closed; rw compl_univ; exact is_open_empty
id └────────┘ └───────────┘
src └──────────────┘ └─┘└────────┘ └────┘└───────────┘└
typ └──────────────┘ └─┘└────────┘ └────┘└───────────┘└
doc └──────────────┘ └─┘ └────┘ └
txt └──────────────┘ └─┘ └────┘ └
par └──────────────┘ └─┘ └────┘ └
pid └────────┘ ┴ ┴ └
st └────────────────────┘└────────┘└─────────────────────
133
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
134 lemma is_closed_union : is_closed s₁ → is_closed s₂ → is_closed (s₁ ∪ s₂) :=
id └───────┘ └┘ └───────┘ └┘ └───────┘ └┘ ┴ └┘
src └───────┘ └───────┘ └───────┘ ┴
typ └───────┘ └┘ └───────┘ └┘ └───────┘ └┘ ┴ └┘
doc └───────┘ └───────┘ └───────┘
135 λ h₁ h₂, by unfold is_closed; rw compl_union; exact is_open_inter h₁ h₂
id └┘ └┘ └─────────┘ └───────────┘ └┘ └┘
src └──────────────┘ └─┘└─────────┘ └────┘└───────────┘┴ ┴ └
typ └┘ └┘ └──────────────┘ └─┘└─────────┘ └────┘└───────────┘┴└┘┴└┘└
doc └──────────────┘ └─┘ └────┘ ┴ ┴ └
txt └──────────────┘ └─┘ └────┘ ┴ ┴ └
par └──────────────┘ └─┘ └────┘ ┴ ┴ └
pid └────────┘ ┴ ┴ ┴ ┴ └
st └────────────────────┘└─────────┘└───────────────────────────
136
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
137 lemma is_closed_sInter {s : set (set α)} : (∀t ∈ s, is_closed t) → is_closed (⋂₀ s) :=
id └─┘ └─┘ ┴ ┴ ┴ └───────┘ ┴ └───────┘ └┘ ┴
src └─┘ └─┘ └───────┘ └───────┘ └┘
typ └─┘ └─┘ ┴ ┴ ┴ └───────┘ ┴ └───────┘ └┘ ┴
doc └───────┘ └───────┘ └┘
138 by simp only [is_closed, compl_sInter, sUnion_image]; exact assume h, is_open_Union $ assume t, is_open_Union $ assume ht, h t ht
id └───────┘ └──────────┘ └──────────┘ └───────────┘
src └─────────┘└───────┘└┘└──────────┘└┘└──────────┘┴ └────┘ └──┘ ┴ ┴ └──┘└───────────┘┴ ┴ └───┘ ┴ ┴ └
typ └─────────┘└───────┘└┘└──────────┘└┘└──────────┘┴ └────┘ └──┘ ┴ ┴ └──┘└───────────┘┴ ┴ └───┘ ┴ ┴ └
doc └─────────┘└───────┘└┘ └┘ ┴ └────┘ └──┘ ┴ ┴ └──┘ ┴ ┴ └───┘ ┴ ┴ └
txt └─────────┘ └┘ └┘ ┴ └────┘ └──┘ ┴ ┴ └──┘ ┴ ┴ └───┘ ┴ ┴ └
par └─────────┘ └┘ └┘ ┴ └────┘ └──┘ ┴ ┴ └──┘ ┴ ┴ └───┘ ┴ ┴ └
pid ┴└──┘└┘ └┘ └┘ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ └───┘ ┴ ┴ └
st └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
139
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
140 lemma is_closed_Inter {f : ι → set α} (h : ∀i, is_closed (f i)) : is_closed (⋂i, f i ) :=
id ┴ └─┘ ┴ ┴ └───────┘ ┴ ┴ └───────┘ ┴┴┴ ┴ ┴
src └─┘ └───────┘ └───────┘ ┴ ┴
typ ┴ └─┘ ┴ ┴ └───────┘ ┴ ┴ └───────┘ ┴┴┴ ┴ ┴
doc └───────┘ └───────┘ ┴ ┴
141 is_closed_sInter $ assume t ⟨i, (heq : f i = t)⟩, heq ▸ h i
id └──────────────┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────────────┘ ┴ ┴ ┴
typ └──────────────┘ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
142
143 @[simp] lemma is_open_compl_iff {s : set α} : is_open (-s) ↔ is_closed s := iff.rfl
id └─┘ ┴ └─────┘ ┴┴ ┴ └───────┘ ┴ └─────┘
src └─┘ └─────┘ ┴ ┴ └───────┘ └─────┘
typ └─┘ ┴ └─────┘ ┴┴ ┴ └───────┘ ┴ └─────┘
doc └──┘ └─────┘ └───────┘
144
145 @[simp] lemma is_closed_compl_iff {s : set α} : is_closed (-s) ↔ is_open s :=
id └─┘ ┴ └───────┘ ┴┴ ┴ └─────┘ ┴
src └─┘ └───────┘ ┴ ┴ └─────┘
typ └─┘ ┴ └───────┘ ┴┴ ┴ └─────┘ ┴
doc └──┘ └───────┘ └─────┘
146 by rw [←is_open_compl_iff, compl_compl]
id └───────────────┘ └─────────┘
src └───┘└───────────────┘└┘└─────────┘└─
typ └───┘└───────────────┘└┘└─────────┘└─
doc └───┘ └┘ └─
txt └───┘ └┘ └─
par └───┘ └┘ └─
pid └─┘ └┘ ┴└
st └─────────────────────┘└───────────┘┴└
147
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
148 lemma is_open_diff {s t : set α} (h₁ : is_open s) (h₂ : is_closed t) : is_open (s \ t) :=
id └─┘ ┴ └─────┘ ┴ └───────┘ ┴ └─────┘ ┴ ┴ ┴
src └─┘ └─────┘ └───────┘ └─────┘ ┴
typ └─┘ ┴ └─────┘ ┴ └───────┘ ┴ └─────┘ ┴ ┴ ┴
doc └─────┘ └───────┘ └─────┘
149 is_open_inter h₁ $ is_open_compl_iff.mpr h₂
id └───────────┘ └┘ └───────────────┘└──┘ └┘
src └───────────┘ └───────────────┘└──┘
typ └───────────┘ └┘ └───────────────┘└──┘ └┘
150
151 lemma is_closed_inter (h₁ : is_closed s₁) (h₂ : is_closed s₂) : is_closed (s₁ ∩ s₂) :=
id └───────┘ └┘ └───────┘ └┘ └───────┘ └┘ ┴ └┘
src └───────┘ └───────┘ └───────┘ ┴
typ └───────┘ └┘ └───────┘ └┘ └───────┘ └┘ ┴ └┘
doc └───────┘ └───────┘ └───────┘
152 by rw [is_closed, compl_inter]; exact is_open_union h₁ h₂
id └───────┘ └─────────┘ └───────────┘ └┘ └┘
src └──┘└───────┘└┘└─────────┘┴ └────┘└───────────┘┴ ┴ └
typ └──┘└───────┘└┘└─────────┘┴ └────┘└───────────┘┴└┘┴└┘└
doc └──┘└───────┘└┘ ┴ └────┘ ┴ ┴ └
txt └──┘ └┘ ┴ └────┘ ┴ ┴ └
par └──┘ └┘ ┴ └────┘ ┴ ┴ └
pid └┘ └┘ ┴ ┴ ┴ ┴ └
st └────────────┘└───────────┘┴└───────────────────────────
153
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
154 lemma is_closed_bUnion {s : set β} {f : β → set α} (hs : finite s) :
id └─┘ ┴ ┴ └─┘ ┴ └────┘ ┴
src └─┘ └─┘ └────┘
typ └─┘ ┴ ┴ └─┘ ┴ └────┘ ┴
doc └────┘
155 (∀i∈s, is_closed (f i)) → is_closed (⋃i∈s, f i) :=
id ┴ ┴ └───────┘ ┴ ┴ └───────┘ ┴┴ ┴┴ ┴ ┴
src └───────┘ └───────┘ ┴ ┴
typ ┴ ┴ └───────┘ ┴ ┴ └───────┘ ┴┴ ┴┴ ┴ ┴
doc └───────┘ └───────┘ ┴ ┴
156 finite.induction_on hs
id └─────────────────┘ └┘
src └─────────────────┘
typ └─────────────────┘ └┘
157 (λ _, by rw bUnion_empty; exact is_closed_empty)
id ┴ └──────────┘ └─────────────┘
src └─┘└──────────┘ └────┘└─────────────┘
typ ┴ └─┘└──────────┘ └────┘└─────────────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ ┴
st └─────────────────────────────────────┘
158 (λ a s has hs ih h, by rw bUnion_insert; exact
id ┴ ┴ └─┘ └┘ └┘ ┴ └───────────┘
src └─┘└───────────┘ └─────
typ ┴ ┴ └─┘ └┘ └┘ ┴ └─┘└───────────┘ └─────
doc └─┘ └─────
txt └─┘ └─────
par └─┘ └─────
pid ┴ └
st └────────────────────────
159 is_closed_union (h a (mem_insert _ _)) (ih (λ i hi, h i (mem_insert_of_mem _ hi))))
id └─────────────┘ ┴ └────────┘ └┘ ┴ └───────────────┘
src ───┘└─────────────┘┴ ┴ ┴ └────────┘└─────┘ ┴ └─────┘ ┴ ┴ └───────────────┘└─┘ └─┘
typ ───┘└─────────────┘┴ ┴┴┴ └────────┘└─────┘ └┘┴ └─────┘┴┴ ┴ └───────────────┘└─┘ └─┘
doc ───┘ ┴ ┴ ┴ └─────┘ ┴ └─────┘ ┴ ┴ └─┘ └─┘
txt ───┘ ┴ ┴ ┴ └─────┘ ┴ └─────┘ ┴ ┴ └─┘ └─┘
par ───┘ ┴ ┴ ┴ └─────┘ ┴ └─────┘ ┴ ┴ └─┘ └─┘
pid ───┘ ┴ ┴ ┴ └─────┘ ┴ └─────┘ ┴ ┴ └─┘ └─┘
st ─────────────────────────────────────────────────────────────────────────────────────┘
160
161 lemma is_closed_Union [fintype β] {s : β → set α}
id └─────┘ ┴ ┴ └─┘ ┴
src └─────┘ └─┘
typ └─────┘ ┴ ┴ └─┘ ┴
doc └─────┘
162 (h : ∀ i, is_closed (s i)) : is_closed (Union s) :=
id ┴ └───────┘ ┴ ┴ └───────┘ └───┘ ┴
src └───────┘ └───────┘ └───┘
typ ┴ └───────┘ ┴ ┴ └───────┘ └───┘ ┴
doc └───────┘ └───────┘ └───┘
163 suffices is_closed (⋃ (i : β) (hi : i ∈ @univ β), s i),
id └───────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
src └───────┘ ┴ ┴ └──┘ ┴
typ └───────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
doc └───────┘ ┴ ┴
164 by convert this; simp [set.ext_iff],
id └──┘ └─────────┘
src └──────┘ └────┘└─────────┘┴
typ └──────┘└──┘ └────┘└─────────┘┴
doc └──────┘ └────┘ ┴
txt └──────┘ └────┘ ┴
par └──────┘ └────┘ ┴
pid ┴ ┴┴ ┴
st └───────────────────────────────┘
165 is_closed_bUnion finite_univ (λ i _, h i)
id └──────────────┘ └─────────┘ ┴ ┴ ┴ ┴
src └──────────────┘ └─────────┘
typ └──────────────┘ └─────────┘ ┴ ┴ ┴ ┴
166
167 lemma is_closed_Union_prop {p : Prop} {s : p → set α}
id ┴ └─┘ ┴
src └─┘
typ ┴ └─┘ ┴
168 (h : ∀ h : p, is_closed (s h)) : is_closed (Union s) :=
id ┴ └───────┘ ┴ ┴ └───────┘ └───┘ ┴
src └───────┘ └───────┘ └───┘
typ ┴ └───────┘ ┴ ┴ └───────┘ └───┘ ┴
doc └───────┘ └───────┘ └───┘
169 by by_cases p; simp *
id ┴
src └───────┘ └──────
typ └───────┘┴ └──────
doc └───────┘ └──────
txt └───────┘ └──────
par └───────┘ └──────
pid ┴ ┴┴└
st └───────────────────
170
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
171 lemma is_closed_imp {p q : α → Prop} (hp : is_open {x | p x})
id ┴ └─────┘ ┴┴ ┴ ┴
src └─────┘ ┴
typ ┴ └─────┘ ┴┴ ┴ ┴
doc └─────┘
172 (hq : is_closed {x | q x}) : is_closed {x | p x → q x} :=
id └───────┘ ┴┴ ┴ ┴ └───────┘ ┴┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ └───────┘ ┴
typ └───────┘ ┴┴ ┴ ┴ └───────┘ ┴┴ ┴ ┴ ┴ ┴
doc └───────┘ └───────┘
173 have {x | p x → q x} = (- {x | p x}) ∪ {x | q x}, from set.ext $ λ x, imp_iff_not_or,
id ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └─────┘ ┴ └────────────┘
src ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ └────────────┘
typ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └─────┘ ┴ └────────────┘
174 by rw [this]; exact is_closed_union (is_closed_compl_iff.mpr hp) hq
id └──┘ └─────────────┘ └─────────────────────┘ └┘ └┘
src └──┘ ┴ └────┘└─────────────┘┴ └─────────────────────┘┴ └┘ └
typ └──┘└──┘┴ └────┘└─────────────┘┴ └─────────────────────┘┴└┘└┘└┘└
doc └──┘ ┴ └────┘ ┴ ┴ └┘ └
txt └──┘ ┴ └────┘ ┴ ┴ └┘ └
par └──┘ ┴ └────┘ ┴ ┴ └┘ └
pid └┘ ┴ ┴ ┴ ┴ └┘ └
st └───────┘┴└───────────────────────────────────────────────────────
175
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
176 lemma is_open_neg : is_closed {a | p a} → is_open {a | ¬ p a} :=
id └───────┘ ┴┴ ┴ ┴ └─────┘ ┴┴ ┴ ┴ ┴
src └───────┘ ┴ └─────┘ ┴ ┴
typ └───────┘ ┴┴ ┴ ┴ └─────┘ ┴┴ ┴ ┴ ┴
doc └───────┘ └─────┘
177 is_open_compl_iff.mpr
id └───────────────┘└──┘
src └───────────────┘└──┘
typ └───────────────┘└──┘
178
179 /-- The interior of a set `s` is the largest open subset of `s`. -/
180 def interior (s : set α) : set α := ⋃₀ {t | is_open t ∧ t ⊆ s}
id └─┘ ┴ └─┘ ┴ └┘ ┴┴ └─────┘ ┴ ┴ ┴ ┴ ┴
src └─┘ └─┘ └┘ ┴ └─────┘ ┴ ┴
typ └─┘ ┴ └─┘ ┴ └┘ ┴┴ └─────┘ ┴ ┴ ┴ ┴ ┴
doc └─────┘
181
182 lemma mem_interior {s : set α} {x : α} :
id └─┘ ┴ ┴
src └─┘
typ └─┘ ┴ ┴
183 x ∈ interior s ↔ ∃ t ⊆ s, is_open t ∧ x ∈ t :=
id ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴┴ └─────┘ ┴ ┴ ┴ ┴ ┴
src ┴ └──────┘ ┴ ┴ ┴ └─────┘ ┴ ┴
typ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴┴ └─────┘ ┴ ┴ ┴ ┴ ┴
doc └──────┘ └─────┘
184 by simp only [interior, mem_set_of_eq, exists_prop, and_assoc, and.left_comm]
id └──────┘ └───────────┘ └─────────┘ └───────┘ └───────────┘
src └─────────┘└──────┘└┘└───────────┘└┘└─────────┘└┘└───────┘└┘└───────────┘└─
typ └─────────┘└──────┘└┘└───────────┘└┘└─────────┘└┘└───────┘└┘└───────────┘└─
doc └─────────┘└──────┘└┘ └┘ └┘ └┘ └─
txt └─────────┘ └┘ └┘ └┘ └┘ └─
par └─────────┘ └┘ └┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ ┴└
st └───────────────────────────────────────────────────────────────────────────
185
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
186 @[simp] lemma is_open_interior {s : set α} : is_open (interior s) :=
id └─┘ ┴ └─────┘ └──────┘ ┴
src └─┘ └─────┘ └──────┘
typ └─┘ ┴ └─────┘ └──────┘ ┴
doc └──┘ └─────┘ └──────┘
187 is_open_sUnion $ assume t ⟨h₁, h₂⟩, h₁
id └────────────┘ ┴ ┴└┘
src └────────────┘
typ └────────────┘ ┴ ┴└┘
188
189 lemma interior_subset {s : set α} : interior s ⊆ s :=
id └─┘ ┴ └──────┘ ┴ ┴ ┴
src └─┘ └──────┘ ┴
typ └─┘ ┴ └──────┘ ┴ ┴ ┴
doc └──────┘
190 sUnion_subset $ assume t ⟨h₁, h₂⟩, h₂
id └───────────┘ ┴ ┴ └┘
src └───────────┘
typ └───────────┘ ┴ ┴ └┘
191
192 lemma interior_maximal {s t : set α} (h₁ : t ⊆ s) (h₂ : is_open t) : t ⊆ interior s :=
id └─┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └──────┘ ┴
src └─┘ ┴ └─────┘ ┴ └──────┘
typ └─┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └──────┘ ┴
doc └─────┘ └──────┘
193 subset_sUnion_of_mem ⟨h₂, h₁⟩
id └──────────────────┘ └┘ └┘
src └──────────────────┘
typ └──────────────────┘ └┘ └┘
194
195 lemma interior_eq_of_open {s : set α} (h : is_open s) : interior s = s :=
id └─┘ ┴ └─────┘ ┴ └──────┘ ┴ ┴ ┴
src └─┘ └─────┘ └──────┘ ┴
typ └─┘ ┴ └─────┘ ┴ └──────┘ ┴ ┴ ┴
doc └─────┘ └──────┘
196 subset.antisymm interior_subset (interior_maximal (subset.refl s) h)
id └─────────────┘ └─────────────┘ └──────────────┘ └─────────┘ ┴ ┴
src └─────────────┘ └─────────────┘ └──────────────┘ └─────────┘
typ └─────────────┘ └─────────────┘ └──────────────┘ └─────────┘ ┴ ┴
197
198 lemma interior_eq_iff_open {s : set α} : interior s = s ↔ is_open s :=
id └─┘ ┴ └──────┘ ┴ ┴ ┴ ┴ └─────┘ ┴
src └─┘ └──────┘ ┴ ┴ └─────┘
typ └─┘ ┴ └──────┘ ┴ ┴ ┴ ┴ └─────┘ ┴
doc └──────┘ └─────┘
199 ⟨assume h, h ▸ is_open_interior, interior_eq_of_open⟩
id ┴ ┴ ┴ └──────────────┘ └─────────────────┘
src ┴ └──────────────┘ └─────────────────┘
typ ┴ ┴ ┴ └──────────────┘ └─────────────────┘
200
201 lemma subset_interior_iff_open {s : set α} : s ⊆ interior s ↔ is_open s :=
id └─┘ ┴ ┴ ┴ └──────┘ ┴ ┴ └─────┘ ┴
src └─┘ ┴ └──────┘ ┴ └─────┘
typ └─┘ ┴ ┴ ┴ └──────┘ ┴ ┴ └─────┘ ┴
doc └──────┘ └─────┘
202 by simp only [interior_eq_iff_open.symm, subset.antisymm_iff, interior_subset, true_and]
id └─────────────────┘ └─────────────┘ └──────┘
src └─────────┘ └┘└─────────────────┘└┘└─────────────┘└┘└──────┘└─
typ └─────────┘└───────────────────────┘└┘└─────────────────┘└┘└─────────────┘└┘└──────┘└─
doc └─────────┘ └┘ └┘ └┘ └─
txt └─────────┘ └┘ └┘ └┘ └─
par └─────────┘ └┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ └┘ ┴└
st └──────────────────────────────────────────────────────────────────────────────────────
203
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
204 lemma subset_interior_iff_subset_of_open {s t : set α} (h₁ : is_open s) :
id └─┘ ┴ └─────┘ ┴
src └─┘ └─────┘
typ └─┘ ┴ └─────┘ ┴
doc └─────┘
205 s ⊆ interior t ↔ s ⊆ t :=
id ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
src ┴ └──────┘ ┴ ┴
typ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
doc └──────┘
206 ⟨assume h, subset.trans h interior_subset, assume h₂, interior_maximal h₂ h₁⟩
id ┴ └──────────┘ ┴ └─────────────┘ └┘ └──────────────┘ └┘ └┘
src └──────────┘ └─────────────┘ └──────────────┘
typ ┴ └──────────┘ ┴ └─────────────┘ └┘ └──────────────┘ └┘ └┘
207
208 lemma interior_mono {s t : set α} (h : s ⊆ t) : interior s ⊆ interior t :=
id └─┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴
src └─┘ ┴ └──────┘ ┴ └──────┘
typ └─┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴
doc └──────┘ └──────┘
209 interior_maximal (subset.trans interior_subset h) is_open_interior
id └──────────────┘ └──────────┘ └─────────────┘ ┴ └──────────────┘
src └──────────────┘ └──────────┘ └─────────────┘ └──────────────┘
typ └──────────────┘ └──────────┘ └─────────────┘ ┴ └──────────────┘
210
211 @[simp] lemma interior_empty : interior (∅ : set α) = ∅ :=
id └──────┘ ┴ └─┘ ┴ ┴ ┴
src └──────┘ ┴ └─┘ ┴ ┴
typ └──────┘ ┴ └─┘ ┴ ┴ ┴
doc └──┘ └──────┘
212 interior_eq_of_open is_open_empty
id └─────────────────┘ └───────────┘
src └─────────────────┘ └───────────┘
typ └─────────────────┘ └───────────┘
213
214 @[simp] lemma interior_univ : interior (univ : set α) = univ :=
id └──────┘ └──┘ └─┘ ┴ ┴ └──┘
src └──────┘ └──┘ └─┘ ┴ └──┘
typ └──────┘ └──┘ └─┘ ┴ ┴ └──┘
doc └──┘ └──────┘
215 interior_eq_of_open is_open_univ
id └─────────────────┘ └──────────┘
src └─────────────────┘ └──────────┘
typ └─────────────────┘ └──────────┘
216
217 @[simp] lemma interior_interior {s : set α} : interior (interior s) = interior s :=
id └─┘ ┴ └──────┘ └──────┘ ┴ ┴ └──────┘ ┴
src └─┘ └──────┘ └──────┘ ┴ └──────┘
typ └─┘ ┴ └──────┘ └──────┘ ┴ ┴ └──────┘ ┴
doc └──┘ └──────┘ └──────┘ └──────┘
218 interior_eq_of_open is_open_interior
id └─────────────────┘ └──────────────┘
src └─────────────────┘ └──────────────┘
typ └─────────────────┘ └──────────────┘
219
220 @[simp] lemma interior_inter {s t : set α} : interior (s ∩ t) = interior s ∩ interior t :=
id └─┘ ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴
src └─┘ └──────┘ ┴ ┴ └──────┘ ┴ └──────┘
typ └─┘ ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └──────┘ ┴
doc └──┘ └──────┘ └──────┘ └──────┘
221 subset.antisymm
id └─────────────┘
src └─────────────┘
typ └─────────────┘
222 (subset_inter (interior_mono $ inter_subset_left s t) (interior_mono $ inter_subset_right s t))
id └──────────┘ └───────────┘ └───────────────┘ ┴ ┴ └───────────┘ └────────────────┘ ┴ ┴
src └──────────┘ └───────────┘ └───────────────┘ └───────────┘ └────────────────┘
typ └──────────┘ └───────────┘ └───────────────┘ ┴ ┴ └───────────┘ └────────────────┘ ┴ ┴
223 (interior_maximal (inter_subset_inter interior_subset interior_subset) $ is_open_inter is_open_interior is_open_interior)
id └──────────────┘ └────────────────┘ └─────────────┘ └─────────────┘ └───────────┘ └──────────────┘ └──────────────┘
src └──────────────┘ └────────────────┘ └─────────────┘ └─────────────┘ └───────────┘ └──────────────┘ └──────────────┘
typ └──────────────┘ └────────────────┘ └─────────────┘ └─────────────┘ └───────────┘ └──────────────┘ └──────────────┘
224
225 lemma interior_union_is_closed_of_interior_empty {s t : set α} (h₁ : is_closed s) (h₂ : interior t = ∅) :
id └─┘ ┴ └───────┘ ┴ └──────┘ ┴ ┴ ┴
src └─┘ └───────┘ └──────┘ ┴ ┴
typ └─┘ ┴ └───────┘ ┴ └──────┘ ┴ ┴ ┴
doc └───────┘ └──────┘
226 interior (s ∪ t) = interior s :=
id └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴
src └──────┘ ┴ ┴ └──────┘
typ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴
doc └──────┘ └──────┘
227 have interior (s ∪ t) ⊆ s, from
id └──────┘ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ ┴
typ └──────┘ ┴ ┴ ┴ ┴ ┴
doc └──────┘
228 assume x ⟨u, ⟨(hu₁ : is_open u), (hu₂ : u ⊆ s ∪ t)⟩, (hx₁ : x ∈ u)⟩,
id ┴ ┴┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ ┴
typ ┴ ┴┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘
229 classical.by_contradiction $ assume hx₂ : x ∉ s,
id └────────────────────────┘ ┴ ┴ ┴
src └────────────────────────┘ ┴
typ └────────────────────────┘ ┴ ┴ ┴
230 have u \ s ⊆ t,
id ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴
231 from assume x ⟨h₁, h₂⟩, or.resolve_left (hu₂ h₁) h₂,
id ┴ ┴└┘ └┘ └─────────────┘
src └─────────────┘
typ ┴ ┴└┘ └┘ └─────────────┘
232 have u \ s ⊆ interior t,
id ┴ ┴ ┴ └──────┘ ┴
src ┴ ┴ └──────┘
typ ┴ ┴ ┴ └──────┘ ┴
doc └──────┘
233 by rwa subset_interior_iff_subset_of_open (is_open_diff hu₁ h₁),
id └────────────────────────────────┘ └──────────┘ └─┘ └┘
src └──┘└────────────────────────────────┘┴ └──────────┘┴ ┴ ┴
typ └──┘└────────────────────────────────┘┴ └──────────┘┴└─┘┴└┘┴
doc └──┘ ┴ ┴ ┴ ┴
txt └──┘ ┴ ┴ ┴ ┴
par └──┘ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴
st └───────────────────────────────────────────────────────────┘
234 have u \ s ⊆ ∅,
id ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
235 by rwa h₂ at this,
id └┘
src └──┘ └──────┘
typ └──┘└┘└──────┘
doc └──┘ └──────┘
txt └──┘ └──────┘
par └──┘ └──────┘
pid ┴ └──────┘
st └─────────────┘
236 this ⟨hx₁, hx₂⟩,
id └──┘ └─┘
typ └──┘ └─┘
237 subset.antisymm
id └─────────────┘
src └─────────────┘
typ └─────────────┘
238 (interior_maximal this is_open_interior)
id └──────────────┘ └──┘ └──────────────┘
src └──────────────┘ └──────────────┘
typ └──────────────┘ └──┘ └──────────────┘
239 (interior_mono $ subset_union_left _ _)
id └───────────┘ └───────────────┘
src └───────────┘ └───────────────┘
typ └───────────┘ └───────────────┘
240
241 lemma is_open_iff_forall_mem_open : is_open s ↔ ∀ x ∈ s, ∃ t ⊆ s, is_open t ∧ x ∈ t :=
id └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ └─────┘ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ ┴ └─────┘ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ └─────┘ ┴ ┴ ┴ ┴ ┴
doc └─────┘ └─────┘
242 by rw ← subset_interior_iff_open; simp only [subset_def, mem_interior]
id └──────────────────────┘ └────────┘ └──────────┘
src └───┘└──────────────────────┘ └─────────┘└────────┘└┘└──────────┘└─
typ └───┘└──────────────────────┘ └─────────┘└────────┘└┘└──────────┘└─
doc └───┘ └─────────┘ └┘ └─
txt └───┘ └─────────┘ └┘ └─
par └───┘ └─────────┘ └┘ └─
pid └─┘ ┴└──┘└┘ └┘ ┴└
st └────────────────────────────────────────────────────────────────────
243
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
244 /-- The closure of `s` is the smallest closed set containing `s`. -/
245 def closure (s : set α) : set α := ⋂₀ {t | is_closed t ∧ s ⊆ t}
id └─┘ ┴ └─┘ ┴ └┘ ┴┴ └───────┘ ┴ ┴ ┴ ┴ ┴
src └─┘ └─┘ └┘ ┴ └───────┘ ┴ ┴
typ └─┘ ┴ └─┘ ┴ └┘ ┴┴ └───────┘ ┴ ┴ ┴ ┴ ┴
doc └┘ └───────┘
246
247 @[simp] lemma is_closed_closure {s : set α} : is_closed (closure s) :=
id └─┘ ┴ └───────┘ └─────┘ ┴
src └─┘ └───────┘ └─────┘
typ └─┘ ┴ └───────┘ └─────┘ ┴
doc └──┘ └───────┘ └─────┘
248 is_closed_sInter $ assume t ⟨h₁, h₂⟩, h₁
id └──────────────┘ ┴ ┴└┘
src └──────────────┘
typ └──────────────┘ ┴ ┴└┘
249
250 lemma subset_closure {s : set α} : s ⊆ closure s :=
id └─┘ ┴ ┴ ┴ └─────┘ ┴
src └─┘ ┴ └─────┘
typ └─┘ ┴ ┴ ┴ └─────┘ ┴
doc └─────┘
251 subset_sInter $ assume t ⟨h₁, h₂⟩, h₂
id └───────────┘ ┴ ┴ └┘
src └───────────┘
typ └───────────┘ ┴ ┴ └┘
252
253 lemma closure_minimal {s t : set α} (h₁ : s ⊆ t) (h₂ : is_closed t) : closure s ⊆ t :=
id └─┘ ┴ ┴ ┴ ┴ └───────┘ ┴ └─────┘ ┴ ┴ ┴
src └─┘ ┴ └───────┘ └─────┘ ┴
typ └─┘ ┴ ┴ ┴ ┴ └───────┘ ┴ └─────┘ ┴ ┴ ┴
doc └───────┘ └─────┘
254 sInter_subset_of_mem ⟨h₂, h₁⟩
id └──────────────────┘ └┘ └┘
src └──────────────────┘
typ └──────────────────┘ └┘ └┘
255
256 lemma closure_eq_of_is_closed {s : set α} (h : is_closed s) : closure s = s :=
id └─┘ ┴ └───────┘ ┴ └─────┘ ┴ ┴ ┴
src └─┘ └───────┘ └─────┘ ┴
typ └─┘ ┴ └───────┘ ┴ └─────┘ ┴ ┴ ┴
doc └───────┘ └─────┘
257 subset.antisymm (closure_minimal (subset.refl s) h) subset_closure
id └─────────────┘ └─────────────┘ └─────────┘ ┴ ┴ └────────────┘
src └─────────────┘ └─────────────┘ └─────────┘ └────────────┘
typ └─────────────┘ └─────────────┘ └─────────┘ ┴ ┴ └────────────┘
258
259 lemma closure_eq_iff_is_closed {s : set α} : closure s = s ↔ is_closed s :=
id └─┘ ┴ └─────┘ ┴ ┴ ┴ ┴ └───────┘ ┴
src └─┘ └─────┘ ┴ ┴ └───────┘
typ └─┘ ┴ └─────┘ ┴ ┴ ┴ ┴ └───────┘ ┴
doc └─────┘ └───────┘
260 ⟨assume h, h ▸ is_closed_closure, closure_eq_of_is_closed⟩
id ┴ ┴ ┴ └───────────────┘ └─────────────────────┘
src ┴ └───────────────┘ └─────────────────────┘
typ ┴ ┴ ┴ └───────────────┘ └─────────────────────┘
261
262 lemma closure_subset_iff_subset_of_is_closed {s t : set α} (h₁ : is_closed t) :
id └─┘ ┴ └───────┘ ┴
src └─┘ └───────┘
typ └─┘ ┴ └───────┘ ┴
doc └───────┘
263 closure s ⊆ t ↔ s ⊆ t :=
id └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘
264 ⟨subset.trans subset_closure, assume h, closure_minimal h h₁⟩
id └──────────┘ └────────────┘ ┴ └─────────────┘ ┴ └┘
src └──────────┘ └────────────┘ └─────────────┘
typ └──────────┘ └────────────┘ ┴ └─────────────┘ ┴ └┘
265
266 lemma closure_mono {s t : set α} (h : s ⊆ t) : closure s ⊆ closure t :=
id └─┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴
src └─┘ ┴ └─────┘ ┴ └─────┘
typ └─┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴
doc └─────┘ └─────┘
267 closure_minimal (subset.trans h subset_closure) is_closed_closure
id └─────────────┘ └──────────┘ ┴ └────────────┘ └───────────────┘
src └─────────────┘ └──────────┘ └────────────┘ └───────────────┘
typ └─────────────┘ └──────────┘ ┴ └────────────┘ └───────────────┘
268
269 lemma monotone_closure (α : Type*) [topological_space α] : monotone (@closure α _) :=
id └───────────────┘ ┴ └──────┘ └─────┘ ┴
src └───────────────┘ └──────┘ └─────┘
typ └───────────────┘ ┴ └──────┘ └─────┘ ┴
doc └───────────────┘ └──────┘ └─────┘
270 λ _ _, closure_mono
id ┴ ┴ └──────────┘
src └──────────┘
typ ┴ ┴ └──────────┘
271
272 lemma closure_inter_subset_inter_closure (s t : set α) :
id └─┘ ┴
src └─┘
typ └─┘ ┴
273 closure (s ∩ t) ⊆ closure s ∩ closure t :=
id └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴
src └─────┘ ┴ ┴ └─────┘ ┴ └─────┘
typ └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴
doc └─────┘ └─────┘ └─────┘
274 (monotone_closure α).map_inf_le s t
id └──────────────┘ ┴ └────────┘ ┴ ┴
src └──────────────┘ └────────┘
typ └──────────────┘ ┴ └────────┘ ┴ ┴
275
276 lemma is_closed_of_closure_subset {s : set α} (h : closure s ⊆ s) : is_closed s :=
id └─┘ ┴ └─────┘ ┴ ┴ ┴ └───────┘ ┴
src └─┘ └─────┘ ┴ └───────┘
typ └─┘ ┴ └─────┘ ┴ ┴ ┴ └───────┘ ┴
doc └─────┘ └───────┘
277 by rw subset.antisymm subset_closure h; exact is_closed_closure
id └─────────────┘ └────────────┘ ┴ └───────────────┘
src └─┘└─────────────┘┴└────────────┘┴ └────┘└───────────────┘└
typ └─┘└─────────────┘┴└────────────┘┴┴ └────┘└───────────────┘└
doc └─┘ ┴ ┴ └────┘ └
txt └─┘ ┴ ┴ └────┘ └
par └─┘ ┴ ┴ └────┘ └
pid ┴ ┴ ┴ ┴ └
st └─────────────────────────────────────────────────────────────
278
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
279 @[simp] lemma closure_empty : closure (∅ : set α) = ∅ :=
id └─────┘ ┴ └─┘ ┴ ┴ ┴
src └─────┘ ┴ └─┘ ┴ ┴
typ └─────┘ ┴ └─┘ ┴ ┴ ┴
doc └──┘ └─────┘
280 closure_eq_of_is_closed is_closed_empty
id └─────────────────────┘ └─────────────┘
src └─────────────────────┘ └─────────────┘
typ └─────────────────────┘ └─────────────┘
281
282 lemma closure_empty_iff (s : set α) : closure s = ∅ ↔ s = ∅ :=
id └─┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └─────┘ ┴ ┴ ┴ ┴ ┴
typ └─┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘
283 ⟨subset_eq_empty subset_closure, λ h, h.symm ▸ closure_empty⟩
id └─────────────┘ └────────────┘ ┴ ┴└───┘ ┴ └───────────┘
src └─────────────┘ └────────────┘ └───┘ ┴ └───────────┘
typ └─────────────┘ └────────────┘ ┴ ┴└───┘ ┴ └───────────┘
284
285 @[simp] lemma closure_univ : closure (univ : set α) = univ :=
id └─────┘ └──┘ └─┘ ┴ ┴ └──┘
src └─────┘ └──┘ └─┘ ┴ └──┘
typ └─────┘ └──┘ └─┘ ┴ ┴ └──┘
doc └──┘ └─────┘
286 closure_eq_of_is_closed is_closed_univ
id └─────────────────────┘ └────────────┘
src └─────────────────────┘ └────────────┘
typ └─────────────────────┘ └────────────┘
287
288 @[simp] lemma closure_closure {s : set α} : closure (closure s) = closure s :=
id └─┘ ┴ └─────┘ └─────┘ ┴ ┴ └─────┘ ┴
src └─┘ └─────┘ └─────┘ ┴ └─────┘
typ └─┘ ┴ └─────┘ └─────┘ ┴ ┴ └─────┘ ┴
doc └──┘ └─────┘ └─────┘ └─────┘
289 closure_eq_of_is_closed is_closed_closure
id └─────────────────────┘ └───────────────┘
src └─────────────────────┘ └───────────────┘
typ └─────────────────────┘ └───────────────┘
290
291 @[simp] lemma closure_union {s t : set α} : closure (s ∪ t) = closure s ∪ closure t :=
id └─┘ ┴ └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴
src └─┘ └─────┘ ┴ ┴ └─────┘ ┴ └─────┘
typ └─┘ ┴ └─────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴
doc └──┘ └─────┘ └─────┘ └─────┘
292 subset.antisymm
id └─────────────┘
src └─────────────┘
typ └─────────────┘
293 (closure_minimal (union_subset_union subset_closure subset_closure) $ is_closed_union is_closed_closure is_closed_closure)
id └─────────────┘ └────────────────┘ └────────────┘ └────────────┘ └─────────────┘ └───────────────┘ └───────────────┘
src └─────────────┘ └────────────────┘ └────────────┘ └────────────┘ └─────────────┘ └───────────────┘ └───────────────┘
typ └─────────────┘ └────────────────┘ └────────────┘ └────────────┘ └─────────────┘ └───────────────┘ └───────────────┘
294 ((monotone_closure α).le_map_sup s t)
id └──────────────┘ ┴ └────────┘ ┴ ┴
src └──────────────┘ └────────┘
typ └──────────────┘ ┴ └────────┘ ┴ ┴
295
296 lemma interior_subset_closure {s : set α} : interior s ⊆ closure s :=
id └─┘ ┴ └──────┘ ┴ ┴ └─────┘ ┴
src └─┘ └──────┘ ┴ └─────┘
typ └─┘ ┴ └──────┘ ┴ ┴ └─────┘ ┴
doc └──────┘ └─────┘
297 subset.trans interior_subset subset_closure
id └──────────┘ └─────────────┘ └────────────┘
src └──────────┘ └─────────────┘ └────────────┘
typ └──────────┘ └─────────────┘ └────────────┘
298
299 lemma closure_eq_compl_interior_compl {s : set α} : closure s = - interior (- s) :=
id └─┘ ┴ └─────┘ ┴ ┴ ┴ └──────┘ ┴ ┴
src └─┘ └─────┘ ┴ ┴ └──────┘ ┴
typ └─┘ ┴ └─────┘ ┴ ┴ ┴ └──────┘ ┴ ┴
doc └─────┘ └──────┘
300 begin
st └─────
301 unfold interior closure is_closed,
src └───────────────────────────────┘
typ └───────────────────────────────┘
doc └───────────────────────────────┘
txt └───────────────────────────────┘
par └───────────────────────────────┘
pid └─────────────────────────┘
st ──────────────────────────────────┘└─
302 rw [compl_sUnion, compl_image_set_of],
id └──────────┘ └────────────────┘
src └──┘└──────────┘└┘└────────────────┘┴
typ └──┘└──────────┘└┘└────────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ─────────────────┘└──────────────────┘└──
303 simp only [compl_subset_compl]
id └────────────────┘
src └─────────┘└────────────────┘└┘
typ └─────────┘└────────────────┘└┘
doc └─────────┘ └┘
txt └─────────┘ └┘
par └─────────┘ └┘
pid ┴└──┘└┘ ┴┴
st ────────────────────────────────┘
304 end
st └─┘
305
306 @[simp] lemma interior_compl {s : set α} : interior (- s) = - closure s :=
id └─┘ ┴ └──────┘ ┴ ┴ ┴ ┴ └─────┘ ┴
src └─┘ └──────┘ ┴ ┴ ┴ └─────┘
typ └─┘ ┴ └──────┘ ┴ ┴ ┴ ┴ └─────┘ ┴
doc └──┘ └──────┘ └─────┘
307 by simp [closure_eq_compl_interior_compl]
id └─────────────────────────────┘
src └────┘└─────────────────────────────┘└─
typ └────┘└─────────────────────────────┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └───────────────────────────────────────
308
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
309 @[simp] lemma closure_compl {s : set α} : closure (- s) = - interior s :=
id └─┘ ┴ └─────┘ ┴ ┴ ┴ ┴ └──────┘ ┴
src └─┘ └─────┘ ┴ ┴ ┴ └──────┘
typ └─┘ ┴ └─────┘ ┴ ┴ ┴ ┴ └──────┘ ┴
doc └──┘ └─────┘ └──────┘
310 by simp [closure_eq_compl_interior_compl]
id └─────────────────────────────┘
src └────┘└─────────────────────────────┘└─
typ └────┘└─────────────────────────────┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └───────────────────────────────────────
311
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
312 theorem mem_closure_iff {s : set α} {a : α} :
id └─┘ ┴ ┴
src └─┘
typ └─┘ ┴ ┴
313 a ∈ closure s ↔ ∀ o, is_open o → a ∈ o → (o ∩ s).nonempty :=
id ┴ ┴ └─────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘
src ┴ └─────┘ ┴ └─────┘ ┴ ┴ └──────┘
typ ┴ ┴ └─────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘
doc └─────┘ └─────┘ └──────┘
314 ⟨λ h o oo ao, classical.by_contradiction $ λ os,
id ┴ ┴ └┘ └┘ └────────────────────────┘ └┘
src └────────────────────────┘
typ ┴ ┴ └┘ └┘ └────────────────────────┘ └┘
315 have s ⊆ -o, from λ x xs xo, os ⟨x, xo, xs⟩,
id ┴ ┴ ┴┴ ┴ └┘ └┘ └┘ ┴ └┘ └┘
src ┴ ┴
typ ┴ ┴ ┴┴ ┴ └┘ └┘ └┘ ┴ └┘ └┘
316 closure_minimal this (is_closed_compl_iff.2 oo) h ao,
id └─────────────┘ └──┘ └─────────────────┘┴ └┘ ┴ └┘
src └─────────────┘ └─────────────────┘┴
typ └─────────────┘ └──┘ └─────────────────┘┴ └┘ ┴ └┘
317 λ H c ⟨h₁, h₂⟩, classical.by_contradiction $ λ nc,
id ┴ ┴ ┴└┘ └┘ └────────────────────────┘ └┘
src └────────────────────────┘
typ ┴ ┴ ┴└┘ └┘ └────────────────────────┘ └┘
318 let ⟨x, hc, hs⟩ := (H _ h₁ nc) in hc (h₂ hs)⟩
id └─┘ └┘ └┘ ┴ └┘
typ └─┘ └┘ └┘ ┴ └┘
319
320 lemma dense_iff_inter_open {s : set α} :
id └─┘ ┴
src └─┘
typ └─┘ ┴
321 closure s = univ ↔ ∀ U, is_open U → U.nonempty → (U ∩ s).nonempty :=
id └─────┘ ┴ ┴ └──┘ ┴ ┴ └─────┘ ┴ ┴└───────┘ ┴ ┴ ┴ └──────┘
src └─────┘ ┴ └──┘ ┴ └─────┘ └───────┘ ┴ └──────┘
typ └─────┘ ┴ ┴ └──┘ ┴ ┴ └─────┘ ┴ ┴└───────┘ ┴ ┴ ┴ └──────┘
doc └─────┘ └─────┘ └───────┘ └──────┘
322 begin
st └─────
323 split ; intro h,
src └────┘ └─────┘
typ └────┘ └─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴ └┘
st ────────────────┘└─
324 { rintros U U_op ⟨x, x_in⟩,
src └──────────────────────┘
typ └──────────────────────┘
doc └──────────────────────┘
txt └──────────────────────┘
par └──────────────────────┘
pid └───────────────┘
st ───┘└──────────────────────┘└─
325 exact mem_closure_iff.1 (by simp only [h]) U U_op x_in },
id └─────────────┘ ┴ ┴ └──┘ └──┘
src └────┘└─────────────┘└─┘ ┴└─────────┘ ┴└┘ ┴ ┴ ┴
typ └────┘└─────────────┘└─┘ ┴└─────────┘┴┴└┘┴┴└──┘┴└──┘┴
doc └────┘ └─┘ ┴└─────────┘ ┴└┘ ┴ ┴ ┴
txt └────┘ └─┘ ┴└─────────┘ ┴└┘ ┴ ┴ ┴
par └────┘ └─┘ ┴└─────────┘ ┴└┘ ┴ ┴ ┴
pid ┴ └─┘ └──────────┘ └─┘ ┴ ┴ ┴
st ──────────────────────────────┘└────────────┘└────────────┘└┘└
326 { apply eq_univ_of_forall, intro x,
id └───────────────┘
src └────┘└───────────────┘ └─────┘
typ └────┘└───────────────┘ └─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴ └┘
st ──────────────────────────┘└───────┘└─
327 rw mem_closure_iff,
id └─────────────┘
src └─┘└─────────────┘
typ └─┘└─────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────────────────────┘└─
328 intros U U_op x_in,
src └────────────────┘
typ └────────────────┘
doc └────────────────┘
txt └────────────────┘
par └────────────────┘
pid └──────────┘
st ─────────────────────┘└─
329 exact h U U_op ⟨_, x_in⟩ },
id ┴ ┴ └──┘ └──┘
src └────┘ ┴ ┴ ┴ └─┘ └┘
typ └────┘┴┴┴┴└──┘┴ └─┘└──┘└┘
doc └────┘ ┴ ┴ ┴ └─┘ └┘
txt └────┘ ┴ ┴ ┴ └─┘ └┘
par └────┘ ┴ ┴ ┴ └─┘ └┘
pid ┴ ┴ ┴ ┴ └─┘ ┴┴
st ────────────────────────────┘└──
330 end
st ──┘
331
332 lemma dense_of_subset_dense {s₁ s₂ : set α} (h : s₁ ⊆ s₂) (hd : closure s₁ = univ) :
id └─┘ ┴ └┘ ┴ └┘ └─────┘ └┘ ┴ └──┘
src └─┘ ┴ └─────┘ ┴ └──┘
typ └─┘ ┴ └┘ ┴ └┘ └─────┘ └┘ ┴ └──┘
doc └─────┘
333 closure s₂ = univ :=
id └─────┘ └┘ ┴ └──┘
src └─────┘ ┴ └──┘
typ └─────┘ └┘ ┴ └──┘
doc └─────┘
334 by { rw [← univ_subset_iff, ← hd], exact closure_mono h }
id └─────────────┘ └┘ └──────────┘ ┴
src └────┘└─────────────┘└──┘ ┴ └────┘└──────────┘┴ ┴
typ └────┘└─────────────┘└──┘└┘┴ └────┘└──────────┘┴┴┴
doc └────┘ └──┘ ┴ └────┘ ┴ ┴
txt └────┘ └──┘ ┴ └────┘ ┴ ┴
par └────┘ └──┘ ┴ └────┘ ┴ ┴
pid └──┘ └──┘ ┴ ┴ ┴ ┴
st └──────────────────────┘└────┘└──────────────────────┘└┘
335
336 /-- The frontier of a set is the set of points between the closure and interior. -/
337 def frontier (s : set α) : set α := closure s \ interior s
id └─┘ ┴ └─┘ ┴ └─────┘ ┴ ┴ └──────┘ ┴
src └─┘ └─┘ └─────┘ ┴ └──────┘
typ └─┘ ┴ └─┘ ┴ └─────┘ ┴ ┴ └──────┘ ┴
doc └─────┘ └──────┘
338
339 lemma frontier_eq_closure_inter_closure {s : set α} :
id └─┘ ┴
src └─┘
typ └─┘ ┴
340 frontier s = closure s ∩ closure (- s) :=
id └──────┘ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴
src └──────┘ ┴ └─────┘ ┴ └─────┘ ┴
typ └──────┘ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴
doc └──────┘ └─────┘ └─────┘
341 by rw [closure_compl, frontier, diff_eq]
id └───────────┘ └──────┘ └─────┘
src └──┘└───────────┘└┘└──────┘└┘└─────┘└─
typ └──┘└───────────┘└┘└──────┘└┘└─────┘└─
doc └──┘ └┘└──────┘└┘ └─
txt └──┘ └┘ └┘ └─
par └──┘ └┘ └┘ └─
pid └┘ └┘ └┘ ┴└
st └────────────────┘└────────┘└───────┘┴└
342
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
343 /-- The complement of a set has the same frontier as the original set. -/
344 @[simp] lemma frontier_compl (s : set α) : frontier (-s) = frontier s :=
id └─┘ ┴ └──────┘ ┴┴ ┴ └──────┘ ┴
src └─┘ └──────┘ ┴ ┴ └──────┘
typ └─┘ ┴ └──────┘ ┴┴ ┴ └──────┘ ┴
doc └──┘ └──────┘ └──────┘
345 by simp only [frontier_eq_closure_inter_closure, lattice.neg_neg, inter_comm]
id └───────────────────────────────┘ └─────────────┘ └────────┘
src └─────────┘└───────────────────────────────┘└┘└─────────────┘└┘└────────┘└─
typ └─────────┘└───────────────────────────────┘└┘└─────────────┘└┘└────────┘└─
doc └─────────┘ └┘ └┘ └─
txt └─────────┘ └┘ └┘ └─
par └─────────┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ ┴└
st └───────────────────────────────────────────────────────────────────────────
346
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
347 lemma frontier_inter_subset (s t : set α) :
id └─┘ ┴
src └─┘
typ └─┘ ┴
348 frontier (s ∩ t) ⊆ (frontier s ∩ closure t) ∪ (closure s ∩ frontier t) :=
id └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴ └──────┘ ┴
src └──────┘ ┴ ┴ └──────┘ ┴ └─────┘ ┴ └─────┘ ┴ └──────┘
typ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴ └──────┘ ┴
doc └──────┘ └──────┘ └─────┘ └─────┘ └──────┘
349 begin
st └─────
350 simp only [frontier_eq_closure_inter_closure, compl_inter, closure_union],
id └───────────────────────────────┘ └─────────┘ └───────────┘
src └─────────┘└───────────────────────────────┘└┘└─────────┘└┘└───────────┘┴
typ └─────────┘└───────────────────────────────┘└┘└─────────┘└┘└───────────┘┴
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st ──────────────────────────────────────────────────────────────────────────┘└─
351 convert inter_subset_inter_left _ (closure_inter_subset_inter_closure s t),
id └─────────────────────┘ └────────────────────────────────┘ ┴ ┴
src └──────┘└─────────────────────┘└─┘ └────────────────────────────────┘┴ ┴ ┴
typ └──────┘└─────────────────────┘└─┘ └────────────────────────────────┘┴┴┴┴┴
doc └──────┘ └─┘ ┴ ┴ ┴
txt └──────┘ └─┘ ┴ ┴ ┴
par └──────┘ └─┘ ┴ ┴ ┴
pid ┴ └─┘ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────────────────┘└─
352 simp only [inter_distrib_left, inter_distrib_right, inter_assoc],
id └────────────────┘ └─────────────────┘ └─────────┘
src └─────────┘└────────────────┘└┘└─────────────────┘└┘└─────────┘┴
typ └─────────┘└────────────────┘└┘└─────────────────┘└┘└─────────┘┴
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st ─────────────────────────────────────────────────────────────────┘└─
353 congr' 2,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid ┴┴
st ─────────┘└─
354 apply inter_comm
id └────────┘
src └────┘└────────┘┴
typ └────┘└────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────┘
355 end
st └─┘
356
357 lemma frontier_union_subset (s t : set α) :
id └─┘ ┴
src └─┘
typ └─┘ ┴
358 frontier (s ∪ t) ⊆ (frontier s ∩ closure (-t)) ∪ (closure (-s) ∩ frontier t) :=
id └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └─────┘ ┴┴ ┴ └─────┘ ┴┴ ┴ └──────┘ ┴
src └──────┘ ┴ ┴ └──────┘ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴ └──────┘
typ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ └─────┘ ┴┴ ┴ └─────┘ ┴┴ ┴ └──────┘ ┴
doc └──────┘ └──────┘ └─────┘ └─────┘ └──────┘
359 by simpa only [frontier_compl, (compl_union _ _).symm]
id └────────────┘ └─────────┘
src └──────────┘└────────────┘└┘ └─────────┘└───────────
typ └──────────┘└────────────┘└┘ └─────────┘└───────────
doc └──────────┘└────────────┘└┘ └───────────
txt └──────────┘ └┘ └───────────
par └──────────┘ └┘ └───────────
pid ┴└──┘└┘ └┘ └─────────┘└
st └────────────────────────────────────────────────────
360 using frontier_inter_subset (-s) (-t)
id └───────────────────┘ ┴┴ ┴
src ───────┘└───────────────────┘┴ ┴ └┘ └─
typ ───────┘└───────────────────┘┴ ┴┴└┘ ┴└─
doc ───────┘ ┴ └┘ └─
txt ───────┘ ┴ └┘ └─
par ───────┘ ┴ └┘ └─
pid ─┘└────┘ ┴ └┘ ┴└
st ────────────────────────────────────────
361
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
362 lemma is_closed.frontier_eq {s : set α} (hs : is_closed s) : frontier s = s \ interior s :=
id └─┘ ┴ └───────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴
src └─┘ └───────┘ └──────┘ ┴ ┴ └──────┘
typ └─┘ ┴ └───────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴
doc └───────┘ └──────┘ └──────┘
363 by rw [frontier, closure_eq_of_is_closed hs]
id └──────┘ └─────────────────────┘ └┘
src └──┘└──────┘└┘└─────────────────────┘┴ └─
typ └──┘└──────┘└┘└─────────────────────┘┴└┘└─
doc └──┘└──────┘└┘ ┴ └─
txt └──┘ └┘ ┴ └─
par └──┘ └┘ ┴ └─
pid └┘ └┘ ┴ ┴└
st └───────────┘└──────────────────────────┘┴└
364
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
365 lemma is_open.frontier_eq {s : set α} (hs : is_open s) : frontier s = closure s \ s :=
id └─┘ ┴ └─────┘ ┴ └──────┘ ┴ ┴ └─────┘ ┴ ┴ ┴
src └─┘ └─────┘ └──────┘ ┴ └─────┘ ┴
typ └─┘ ┴ └─────┘ ┴ └──────┘ ┴ ┴ └─────┘ ┴ ┴ ┴
doc └─────┘ └──────┘ └─────┘
366 by rw [frontier, interior_eq_of_open hs]
id └──────┘ └─────────────────┘ └┘
src └──┘└──────┘└┘└─────────────────┘┴ └─
typ └──┘└──────┘└┘└─────────────────┘┴└┘└─
doc └──┘└──────┘└┘ ┴ └─
txt └──┘ └┘ ┴ └─
par └──┘ └┘ ┴ └─
pid └┘ └┘ ┴ ┴└
st └───────────┘└──────────────────────┘┴└
367
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
368 /-- The frontier of a set is closed. -/
369 lemma is_closed_frontier {s : set α} : is_closed (frontier s) :=
id └─┘ ┴ └───────┘ └──────┘ ┴
src └─┘ └───────┘ └──────┘
typ └─┘ ┴ └───────┘ └──────┘ ┴
doc └───────┘ └──────┘
370 by rw frontier_eq_closure_inter_closure; exact is_closed_inter is_closed_closure is_closed_closure
id └───────────────────────────────┘ └─────────────┘ └───────────────┘
src └─┘└───────────────────────────────┘ └────┘└─────────────┘┴ ┴└───────────────┘└
typ └─┘└───────────────────────────────┘ └────┘└─────────────┘┴ ┴└───────────────┘└
doc └─┘ └────┘ ┴ ┴ └
txt └─┘ └────┘ ┴ ┴ └
par └─┘ └────┘ ┴ ┴ └
pid ┴ ┴ ┴ ┴ └
st └────────────────────────────────────────────────────────────────────────────────────────────────
371
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
372 /-- The frontier of a set has no interior point. -/
373 lemma interior_frontier {s : set α} (h : is_closed s) : interior (frontier s) = ∅ :=
id └─┘ ┴ └───────┘ ┴ └──────┘ └──────┘ ┴ ┴ ┴
src └─┘ └───────┘ └──────┘ └──────┘ ┴ ┴
typ └─┘ ┴ └───────┘ ┴ └──────┘ └──────┘ ┴ ┴ ┴
doc └───────┘ └──────┘ └──────┘
374 begin
st └─────
375 have A : frontier s = s \ interior s, from h.frontier_eq,
id └──────┘ ┴ ┴ └──────┘ ┴ └───────────┘
src └───────┘└──────┘┴ ┴┴┴ ┴┴┴└──────┘┴ └───┘└───────────┘
typ └───────┘└──────┘┴ ┴┴┴ ┴┴┴└──────┘┴┴ └───┘└───────────┘
doc └───────┘└──────┘┴ ┴ ┴ ┴ ┴└──────┘┴ └───┘
txt └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘
par └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘
pid └────┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘
st ─────────────────────────────────────┘└──────────────────┘└─
376 have B : interior (frontier s) ⊆ interior s, by rw A; exact interior_mono (diff_subset _ _),
id └──────┘ ┴ └──────┘ ┴ ┴ └───────────┘ └─────────┘
src └───────┘ ┴ └──────┘┴ └┘┴┴└──────┘┴ └─┘ └────┘└───────────┘┴ └─────────┘└───┘
typ └───────┘ ┴ └──────┘┴ └┘┴┴└──────┘┴┴ └─┘┴ └────┘└───────────┘┴ └─────────┘└───┘
doc └───────┘ ┴ └──────┘┴ └┘ ┴└──────┘┴ └─┘ └────┘ ┴ └───┘
txt └───────┘ ┴ ┴ └┘ ┴ ┴ └─┘ └────┘ ┴ └───┘
par └───────┘ ┴ ┴ └┘ ┴ ┴ └─┘ └────┘ ┴ └───┘
pid └────┘└─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └───┘
st ────────────────────────────────────────────┘ ┴ └─
377 have C : interior (frontier s) ⊆ frontier s := interior_subset,
id └──────┘ └──────┘ ┴ └─────────────┘
src └───────┘└──────┘┴ ┴ └┘ ┴└──────┘┴ └──┘└─────────────┘
typ └───────┘└──────┘┴ ┴ └┘ ┴└──────┘┴┴└──┘└─────────────┘
doc └───────┘└──────┘┴ ┴ └┘ ┴└──────┘┴ └──┘
txt └───────┘ ┴ ┴ └┘ ┴ ┴ └──┘
par └───────┘ ┴ ┴ └┘ ┴ ┴ └──┘
pid └────┘└─┘ ┴ ┴ └┘ ┴ ┴ └──┘
st ───────────────────────────────────────────────────────────────┘└─
378 have : interior (frontier s) ⊆ (interior s) ∩ (s \ interior s) :=
id └──────┘ ┴ └──────┘ ┴
src └─────┘ ┴ └──────┘┴ └┘ ┴ ┴ └┘┴┴ ┴ ┴└──────┘┴ └────
typ └─────┘ ┴ └──────┘┴ └┘ ┴ ┴ └┘┴┴ ┴ ┴└──────┘┴┴└────
doc └─────┘ ┴ └──────┘┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴└──────┘┴ └────
txt └─────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └────
par └─────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └────
pid └───┘└┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴└───
st ────────────────────────────────────────────────────────────────────
379 subset_inter B (by simpa [A] using C),
id └──────────┘ ┴ ┴ ┴
src ───┘└──────────┘┴ ┴ ┴└─────┘ └──────┘ ┴
typ ───┘└──────────┘┴┴┴ ┴└─────┘┴└──────┘┴┴
doc ───┘ ┴ ┴ ┴└─────┘ └──────┘ ┴
txt ───┘ ┴ ┴ ┴└─────┘ └──────┘ ┴
par ───┘ ┴ ┴ ┴└─────┘ └──────┘ ┴
pid ───┘ ┴ ┴ └──────┘ └──────┘ ┴
st ─────────────────────┘└────────────────┘┴└─
380 rwa [inter_diff_self, subset_empty_iff] at this,
id └─────────────┘ └──────────────┘
src └───┘└─────────────┘└┘└──────────────┘└───────┘
typ └───┘└─────────────┘└┘└──────────────┘└───────┘
doc └───┘ └┘ └───────┘
txt └───┘ └┘ └───────┘
par └───┘ └┘ └───────┘
pid └┘ └┘ ┴└──────┘
st ─────────────────────┘└────────────────┘┴└──────┘└─
381 end
st ──┘
382
383 /-- neighbourhood filter -/
384 def nhds (a : α) : filter α := (⨅ s ∈ {s : set α | a ∈ s ∧ is_open s}, principal s)
id ┴ └────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └───────┘ ┴
src └────┘ ┴ ┴ └─┘ ┴ ┴ └─────┘ ┴ └───────┘
typ ┴ └────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └───────┘ ┴
doc ┴ └─────┘ ┴ └───────┘
385
386 localized "notation `𝓝` := nhds" in topological_space
387
388 lemma nhds_def (a : α) : 𝓝 a = (⨅ s ∈ {s : set α | a ∈ s ∧ is_open s}, principal s) := rfl
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └───────┘ ┴ └─┘
src ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─────┘ ┴ └───────┘ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └───────┘ ┴ └─┘
doc ┴ ┴ └─────┘ ┴ └───────┘
389
390 lemma le_nhds_iff {f a} : f ≤ 𝓝 a ↔ ∀ s : set α, a ∈ s → is_open s → s ∈ f :=
id ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ └─┘ ┴ └─────┘ ┴
typ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
doc ┴ └─────┘
391 by simp [nhds_def]
id └──────┘
src └────┘└──────┘└─
typ └────┘└──────┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └────────────────
392
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
393 lemma nhds_le_of_le {f a} {s : set α} (h : a ∈ s) (o : is_open s) (sf : principal s ≤ f) : 𝓝 a ≤ f :=
id └─┘ ┴ ┴ ┴ ┴ └─────┘ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ └─────┘ └───────┘ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴ └─────┘ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ └───────┘ ┴
394 by rw nhds_def; exact infi_le_of_le s (infi_le_of_le ⟨h, o⟩ sf)
id └──────┘ ┴ └───────────┘ ┴ ┴ └┘
src └─┘└──────┘ └────┘ ┴ ┴ └───────────┘┴ └┘ └┘ └─
typ └─┘└──────┘ └────┘ ┴┴┴ └───────────┘┴ ┴└┘┴└┘└┘└─
doc └─┘ └────┘ ┴ ┴ ┴ └┘ └┘ └─
txt └─┘ └────┘ ┴ ┴ ┴ └┘ └┘ └─
par └─┘ └────┘ ┴ ┴ ┴ └┘ └┘ └─
pid ┴ ┴ ┴ ┴ ┴ └┘ └┘ ┴└
st └─────────────────────────────────────────────────────────────
395
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
396 lemma nhds_sets {a : α} : (𝓝 a).sets = {s | ∃t⊆s, is_open t ∧ a ∈ t} :=
id ┴ ┴ ┴ └──┘ ┴ ┴┴ ┴┴ ┴┴ └─────┘ ┴ ┴ ┴ ┴ ┴
src ┴ └──┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴
typ ┴ ┴ ┴ └──┘ ┴ ┴┴ ┴┴ ┴┴ └─────┘ ┴ ┴ ┴ ┴ ┴
doc ┴ └─────┘
397 calc (𝓝 a).sets = (⋃s∈{s : set α| a ∈ s ∧ is_open s}, (principal s).sets) : binfi_sets_eq
id ┴ ┴ └──┘ ┴┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └───────┘ ┴ └──┘ └───────────┘
src ┴ └──┘ ┴ ┴ └─┘ ┴ ┴ └─────┘ ┴ └───────┘ └──┘ └───────────┘
typ ┴ ┴ └──┘ ┴┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └───────┘ ┴ └──┘ └───────────┘
doc ┴ ┴ └─────┘ ┴ └───────┘
398 (assume x ⟨hx₁, hx₂⟩ y ⟨hy₁, hy₂⟩,
id ┴ ┴└─┘ └─┘ ┴ ┴└─┘ └─┘
typ ┴ ┴└─┘ └─┘ ┴ ┴└─┘ └─┘
399 ⟨x ∩ y, ⟨⟨hx₁, hy₁⟩, is_open_inter hx₂ hy₂⟩,
id ┴ ┴ ┴ └───────────┘
src ┴ └───────────┘
typ ┴ ┴ ┴ └───────────┘
400 le_principal_iff.2 (inter_subset_left _ _),
id └──────────────┘┴ └───────────────┘
src └──────────────┘┴ └───────────────┘
typ └──────────────┘┴ └───────────────┘
401 le_principal_iff.2 (inter_subset_right _ _)⟩)
id └──────────────┘┴ └────────────────┘
src └──────────────┘┴ └────────────────┘
typ └──────────────┘┴ └────────────────┘
402 ⟨univ, mem_univ _, is_open_univ⟩
id └──┘ └──────┘ └──────────┘
src └──┘ └──────┘ └──────────┘
typ └──┘ └──────┘ └──────────┘
403 ... = {s | ∃t⊆s, is_open t ∧ a ∈ t} :
id ┴┴ ┴┴ ┴┴ └─────┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ └─────┘ ┴ ┴
typ ┴┴ ┴┴ ┴┴ └─────┘ ┴ ┴ ┴ ┴ ┴
doc └─────┘
404 le_antisymm
id └─────────┘
src └─────────┘
typ └─────────┘
405 (supr_le $ assume i, supr_le $ assume ⟨hi₁, hi₂⟩ t ht, ⟨i, ht, hi₂, hi₁⟩)
id └─────┘ ┴ └─────┘ ┴└─┘ └─┘ ┴ └┘ ┴ └┘
src └─────┘ └─────┘
typ └─────┘ ┴ └─────┘ ┴└─┘ └─┘ ┴ └┘ ┴ └┘
406 (assume t ⟨i, hi₁, hi₂, hi₃⟩, mem_Union.2 ⟨i, mem_Union.2 ⟨⟨hi₃, hi₂⟩, hi₁⟩⟩)
id ┴ ┴┴ └─┘ └─┘ └─┘ └───────┘┴ └───────┘┴
src └───────┘┴ └───────┘┴
typ ┴ ┴┴ └─┘ └─┘ └─┘ └───────┘┴ └───────┘┴
407
408 lemma map_nhds {a : α} {f : α → β} :
id ┴ ┴ ┴
typ ┴ ┴ ┴
409 map f (𝓝 a) = (⨅ s ∈ {s : set α | a ∈ s ∧ is_open s}, principal (image f s)) :=
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └───────┘ └───┘ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─────┘ ┴ └───────┘ └───┘
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └───────┘ └───┘ ┴ ┴
doc └─┘ ┴ ┴ └─────┘ ┴ └───────┘
410 calc map f (𝓝 a) = (⨅ s ∈ {s : set α | a ∈ s ∧ is_open s}, map f (principal s)) :
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─┘ ┴ └───────┘ ┴
src └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └─────┘ ┴ └─┘ └───────┘
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─┘ ┴ └───────┘ ┴
doc └─┘ ┴ ┴ └─────┘ ┴ └─┘ └───────┘
411 map_binfi_eq
id └──────────┘
src └──────────┘
typ └──────────┘
412 (assume x ⟨hx₁, hx₂⟩ y ⟨hy₁, hy₂⟩,
id ┴ ┴└─┘ └─┘ ┴ ┴└─┘ └─┘
typ ┴ ┴└─┘ └─┘ ┴ ┴└─┘ └─┘
413 ⟨x ∩ y, ⟨⟨hx₁, hy₁⟩, is_open_inter hx₂ hy₂⟩,
id ┴ ┴ ┴ └───────────┘
src ┴ └───────────┘
typ ┴ ┴ ┴ └───────────┘
414 le_principal_iff.2 (inter_subset_left _ _),
id └──────────────┘┴ └───────────────┘
src └──────────────┘┴ └───────────────┘
typ └──────────────┘┴ └───────────────┘
415 le_principal_iff.2 (inter_subset_right _ _)⟩)
id └──────────────┘┴ └────────────────┘
src └──────────────┘┴ └────────────────┘
typ └──────────────┘┴ └────────────────┘
416 ⟨univ, mem_univ _, is_open_univ⟩
id └──┘ └──────┘ └──────────┘
src └──┘ └──────┘ └──────────┘
typ └──┘ └──────┘ └──────────┘
417 ... = _ : by simp only [map_principal]
id └───────────┘
src └─────────┘└───────────┘└─
typ └─────────┘└───────────┘└─
doc └─────────┘ └─
txt └─────────┘ └─
par └─────────┘ └─
pid ┴└──┘└┘ ┴└
st └──────────────────────────
418
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
419 attribute [irreducible] nhds
id └──┘
src └──┘
typ └──┘
doc └─────────┘ └──┘
420
421 lemma mem_nhds_sets_iff {a : α} {s : set α} :
id ┴ └─┘ ┴
src └─┘
typ ┴ └─┘ ┴
422 s ∈ 𝓝 a ↔ ∃t⊆s, is_open t ∧ a ∈ t :=
id ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ └─────┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ └─────┘ ┴ ┴ ┴ ┴ ┴
doc ┴ └─────┘
423 by simp only [nhds_sets, mem_set_of_eq, exists_prop]
id └───────┘ └───────────┘ └─────────┘
src └─────────┘└───────┘└┘└───────────┘└┘└─────────┘└─
typ └─────────┘└───────┘└┘└───────────┘└┘└─────────┘└─
doc └─────────┘ └┘ └┘ └─
txt └─────────┘ └┘ └┘ └─
par └─────────┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ ┴└
st └──────────────────────────────────────────────────
424
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
425 lemma mem_of_nhds {a : α} {s : set α} : s ∈ 𝓝 a → a ∈ s :=
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
426 λ H, let ⟨t, ht, _, hs⟩ := mem_nhds_sets_iff.1 H in ht hs
id ┴ └─┘ └┘ └┘ └───────────────┘┴ ┴
src └───────────────┘┴
typ ┴ └─┘ └┘ └┘ └───────────────┘┴ ┴
427
428 lemma mem_nhds_sets {a : α} {s : set α} (hs : is_open s) (ha : a ∈ s) :
id ┴ └─┘ ┴ └─────┘ ┴ ┴ ┴ ┴
src └─┘ └─────┘ ┴
typ ┴ └─┘ ┴ └─────┘ ┴ ┴ ┴ ┴
doc └─────┘
429 s ∈ 𝓝 a :=
id ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴
doc ┴
430 mem_nhds_sets_iff.2 ⟨s, subset.refl _, hs, ha⟩
id └───────────────┘┴ ┴ └─────────┘ └┘ └┘
src └───────────────┘┴ └─────────┘
typ └───────────────┘┴ ┴ └─────────┘ └┘ └┘
431
432 theorem all_mem_nhds (x : α) (P : set α → Prop) (hP : ∀ s t, s ⊆ t → P s → P t) :
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
433 (∀ s ∈ 𝓝 x, P s) ↔ (∀ s, is_open s → x ∈ s → P s) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └─────┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ └─────┘
434 iff.intro
id └───────┘
src └───────┘
typ └───────┘
435 (λ h s os xs, h s (mem_nhds_sets os xs))
id ┴ ┴ └┘ └┘ ┴ ┴ └───────────┘ └┘ └┘
src └───────────┘
typ ┴ ┴ └┘ └┘ ┴ ┴ └───────────┘ └┘ └┘
436 (λ h t,
id ┴ ┴
typ ┴ ┴
437 begin
st └─────
438 change t ∈ (𝓝 x).sets → P t,
id ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴┴┴ ┴┴ └─────┘ ┴ ┴
typ └─────┘ ┴┴┴ ┴┴┴└─────┘ ┴┴┴┴
doc └─────┘ ┴ ┴ ┴┴ └─────┘ ┴ ┴
txt └─────┘ ┴ ┴ ┴ └─────┘ ┴ ┴
par └─────┘ ┴ ┴ ┴ └─────┘ ┴ ┴
pid ┴ ┴ ┴ ┴ └─────┘ ┴ ┴
st ────────────────────────────────┘└─
439 rw nhds_sets,
id └───────┘
src └─┘└───────┘
typ └─┘└───────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────────────────┘└─
440 rintros ⟨s, hs, opens, xs⟩,
src └────────────────────────┘
typ └────────────────────────┘
doc └────────────────────────┘
txt └────────────────────────┘
par └────────────────────────┘
pid └─────────────────┘
st ───────────────────────────────┘└─
441 exact hP _ _ hs (h s opens xs),
id └┘ └┘ ┴ ┴ └───┘ └┘
src └────┘ └───┘ ┴ ┴ ┴ ┴ ┴
typ └────┘└┘└───┘└┘┴ ┴┴┴┴└───┘┴└┘┴
doc └────┘ └───┘ ┴ ┴ ┴ ┴ ┴
txt └────┘ └───┘ ┴ ┴ ┴ ┴ ┴
par └────┘ └───┘ ┴ ┴ ┴ ┴ ┴
pid ┴ └───┘ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────┘└─
442 end)
st ──────┘
443
444 theorem all_mem_nhds_filter (x : α) (f : set α → set β) (hf : ∀ s t, s ⊆ t → f s ⊆ f t)
id ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └─┘ ┴ ┴
typ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
445 (l : filter β) :
id └────┘ ┴
src └────┘
typ └────┘ ┴
446 (∀ s ∈ 𝓝 x, f s ∈ l) ↔ (∀ s, is_open s → x ∈ s → f s ∈ l) :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ └─────┘ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ └─────┘
447 all_mem_nhds _ _ (λ s t ssubt h, mem_sets_of_superset h (hf s t ssubt))
id └──────────┘ ┴ ┴ └───┘ ┴ └──────────────────┘ ┴ └┘ ┴ ┴ └───┘
src └──────────┘ └──────────────────┘
typ └──────────┘ ┴ ┴ └───┘ ┴ └──────────────────┘ ┴ └┘ ┴ ┴ └───┘
448
449 theorem rtendsto_nhds {r : rel β α} {l : filter β} {a : α} :
id └─┘ ┴ ┴ └────┘ ┴ ┴
src └─┘ └────┘
typ └─┘ ┴ ┴ └────┘ ┴ ┴
doc └─┘
450 rtendsto r l (𝓝 a) ↔ (∀ s, is_open s → a ∈ s → r.core s ∈ l) :=
id └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴
src └──────┘ ┴ ┴ └─────┘ ┴ └───┘ ┴
typ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴
doc ┴ └─────┘ └───┘
451 all_mem_nhds_filter _ _ (λ s t, id) _
id └─────────────────┘ ┴ ┴ └┘
src └─────────────────┘ └┘
typ └─────────────────┘ ┴ ┴ └┘
452
453 theorem rtendsto'_nhds {r : rel β α} {l : filter β} {a : α} :
id └─┘ ┴ ┴ └────┘ ┴ ┴
src └─┘ └────┘
typ └─┘ ┴ ┴ └────┘ ┴ ┴
doc └─┘
454 rtendsto' r l (𝓝 a) ↔ (∀ s, is_open s → a ∈ s → r.preimage s ∈ l) :=
id └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴└───────┘ ┴ ┴ ┴
src └───────┘ ┴ ┴ └─────┘ ┴ └───────┘ ┴
typ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴└───────┘ ┴ ┴ ┴
doc ┴ └─────┘ └───────┘
455 by { rw [rtendsto'_def], apply all_mem_nhds_filter, apply rel.preimage_mono }
id └───────────┘ └─────────────────┘ └───────────────┘
src └──┘└───────────┘┴ └────┘└─────────────────┘ └────┘└───────────────┘┴
typ └──┘└───────────┘┴ └────┘└─────────────────┘ └────┘└───────────────┘┴
doc └──┘ ┴ └────┘ └────┘ ┴
txt └──┘ ┴ └────┘ └────┘ ┴
par └──┘ ┴ └────┘ └────┘ ┴
pid └┘ ┴ ┴ ┴ ┴
st └──────────────────┘└──────────────────────────┘└────────────────────────┘└┘
456
457 theorem ptendsto_nhds {f : β →. α} {l : filter β} {a : α} :
id ┴ └┘ ┴ └────┘ ┴ ┴
src └┘ └────┘
typ ┴ └┘ ┴ └────┘ ┴ ┴
doc └┘
458 ptendsto f l (𝓝 a) ↔ (∀ s, is_open s → a ∈ s → f.core s ∈ l) :=
id └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴
src └──────┘ ┴ ┴ └─────┘ ┴ └───┘ ┴
typ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴
doc ┴ └─────┘
459 rtendsto_nhds
id └───────────┘
src └───────────┘
typ └───────────┘
460
461 theorem ptendsto'_nhds {f : β →. α} {l : filter β} {a : α} :
id ┴ └┘ ┴ └────┘ ┴ ┴
src └┘ └────┘
typ ┴ └┘ ┴ └────┘ ┴ ┴
doc └┘
462 ptendsto' f l (𝓝 a) ↔ (∀ s, is_open s → a ∈ s → f.preimage s ∈ l) :=
id └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴└───────┘ ┴ ┴ ┴
src └───────┘ ┴ ┴ └─────┘ ┴ └───────┘ ┴
typ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴└───────┘ ┴ ┴ ┴
doc ┴ └─────┘
463 rtendsto'_nhds
id └────────────┘
src └────────────┘
typ └────────────┘
464
465 theorem tendsto_nhds {f : β → α} {l : filter β} {a : α} :
id ┴ ┴ └────┘ ┴ ┴
src └────┘
typ ┴ ┴ └────┘ ┴ ┴
466 tendsto f l (𝓝 a) ↔ (∀ s, is_open s → a ∈ s → f ⁻¹' s ∈ l) :=
id └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
src └─────┘ ┴ ┴ └─────┘ ┴ └─┘ ┴
typ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
doc └─────┘ ┴ └─────┘ └─┘
467 all_mem_nhds_filter _ _ (λ s t h, preimage_mono h) _
id └─────────────────┘ ┴ ┴ ┴ └───────────┘ ┴
src └─────────────────┘ └───────────┘
typ └─────────────────┘ ┴ ┴ ┴ └───────────┘ ┴
468
469 lemma tendsto_const_nhds {a : α} {f : filter β} : tendsto (λb:β, a) f (𝓝 a) :=
id ┴ └────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴
src └────┘ └─────┘ ┴
typ ┴ └────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴
doc └─────┘ ┴
470 tendsto_nhds.mpr $ assume s hs ha, univ_mem_sets' $ assume _, ha
id └──────────┘└──┘ ┴ └┘ └┘ └────────────┘ ┴ └┘
src └──────────┘└──┘ └────────────┘
typ └──────────┘└──┘ ┴ └┘ └┘ └────────────┘ ┴ └┘
471
472 lemma pure_le_nhds : pure ≤ (𝓝 : α → filter α) :=
id └──┘ ┴ ┴ ┴ └────┘ ┴
src └──┘ ┴ ┴ └────┘
typ └──┘ ┴ ┴ ┴ └────┘ ┴
doc ┴
473 assume a s hs, mem_pure_sets.2 $ mem_of_nhds hs
id ┴ ┴ └┘ └───────────┘┴ └─────────┘ └┘
src └───────────┘┴ └─────────┘
typ ┴ ┴ └┘ └───────────┘┴ └─────────┘ └┘
474
475 lemma tendsto_pure_nhds {α : Type*} [topological_space β] (f : α → β) (a : α) :
id └───────────────┘ ┴ ┴ ┴ ┴
src └───────────────┘
typ └───────────────┘ ┴ ┴ ┴ ┴
doc └───────────────┘
476 tendsto f (pure a) (𝓝 (f a)) :=
id └─────┘ ┴ └──┘ ┴ ┴ ┴ ┴
src └─────┘ └──┘ ┴
typ └─────┘ ┴ └──┘ ┴ ┴ ┴ ┴
doc └─────┘ ┴
477 begin
st └─────
478 rw [tendsto, filter.map_pure],
id └─────┘ └─────────────┘
src └──┘└─────┘└┘└─────────────┘┴
typ └──┘└─────┘└┘└─────────────┘┴
doc └──┘└─────┘└┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ────────────┘└───────────────┘└──
479 exact pure_le_nhds (f a)
id └──────────┘ ┴ ┴
src └────┘└──────────┘┴ ┴ └┘
typ └────┘└──────────┘┴ ┴┴┴└┘
doc └────┘ ┴ ┴ └┘
txt └────┘ ┴ ┴ └┘
par └────┘ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴┴
st ──────────────────────────┘
480 end
st └─┘
481
482 @[simp] lemma nhds_ne_bot {a : α} : 𝓝 a ≠ ⊥ :=
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
doc └──┘ ┴
483 ne_bot_of_le_ne_bot pure_ne_bot (pure_le_nhds a)
id └─────────────────┘ └─────────┘ └──────────┘ ┴
src └─────────────────┘ └─────────┘ └──────────┘
typ └─────────────────┘ └─────────┘ └──────────┘ ┴
484
485 lemma interior_eq_nhds {s : set α} : interior s = {a | 𝓝 a ≤ principal s} :=
id └─┘ ┴ └──────┘ ┴ ┴ ┴┴ ┴ ┴ ┴ └───────┘ ┴
src └─┘ └──────┘ ┴ ┴ ┴ ┴ └───────┘
typ └─┘ ┴ └──────┘ ┴ ┴ ┴┴ ┴ ┴ ┴ └───────┘ ┴
doc └──────┘ ┴ └───────┘
486 set.ext $ λ x, by simp only [mem_interior, le_principal_iff, mem_nhds_sets_iff]; refl
id └─────┘ ┴ └──────────┘ └──────────────┘ └───────────────┘
src └─────┘ └─────────┘└──────────┘└┘└──────────────┘└┘└───────────────┘┴ └────
typ └─────┘ ┴ └─────────┘└──────────┘└┘└──────────────┘└┘└───────────────┘┴ └────
doc └─────────┘ └┘ └┘ ┴ └────
txt └─────────┘ └┘ └┘ ┴ └────
par └─────────┘ └┘ └┘ ┴ └────
pid ┴└──┘└┘ └┘ └┘ ┴ └
st └────────────────────────────────────────────────────────────────────
487
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
488 lemma mem_interior_iff_mem_nhds {s : set α} {a : α} :
id └─┘ ┴ ┴
src └─┘
typ └─┘ ┴ ┴
489 a ∈ interior s ↔ s ∈ 𝓝 a :=
id ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └──────┘ ┴ ┴ ┴
typ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──────┘ ┴
490 by simp only [interior_eq_nhds, le_principal_iff]; refl
id └──────────────┘ └──────────────┘
src └─────────┘└──────────────┘└┘└──────────────┘┴ └────
typ └─────────┘└──────────────┘└┘└──────────────┘┴ └────
doc └─────────┘ └┘ ┴ └────
txt └─────────┘ └┘ ┴ └────
par └─────────┘ └┘ ┴ └────
pid ┴└──┘└┘ └┘ ┴ └
st └─────────────────────────────────────────────────────
491
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
492 lemma is_open_iff_nhds {s : set α} : is_open s ↔ ∀a∈s, 𝓝 a ≤ principal s :=
id └─┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴
src └─┘ └─────┘ ┴ ┴ ┴ └───────┘
typ └─┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴
doc └─────┘ ┴ └───────┘
493 calc is_open s ↔ s ⊆ interior s : subset_interior_iff_open.symm
id └─────┘ ┴ ┴ ┴ └──────┘ ┴ └──────────────────────┘└───┘
src └─────┘ ┴ └──────┘ └──────────────────────┘└───┘
typ └─────┘ ┴ ┴ ┴ └──────┘ ┴ └──────────────────────┘└───┘
doc └─────┘ └──────┘
494 ... ↔ (∀a∈s, 𝓝 a ≤ principal s) : by rw [interior_eq_nhds]; refl
id ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ └──────────────┘
src ┴ ┴ └───────┘ └──┘└──────────────┘┴ └────
typ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ └──┘└──────────────┘┴ └────
doc ┴ └───────┘ └──┘ ┴ └────
txt └──┘ ┴ └────
par └──┘ ┴ └────
pid └┘ ┴ └
st └───────────────────┘┴└──────
495
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
496 lemma is_open_iff_mem_nhds {s : set α} : is_open s ↔ ∀a∈s, s ∈ 𝓝 a :=
id └─┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └─────┘ ┴ ┴ ┴
typ └─┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ ┴
497 is_open_iff_nhds.trans $ forall_congr $ λ _, imp_congr_right $ λ _, le_principal_iff
id └──────────────┘└────┘ └──────────┘ ┴ └─────────────┘ ┴ └──────────────┘
src └──────────────┘└────┘ └──────────┘ └─────────────┘ └──────────────┘
typ └──────────────┘└────┘ └──────────┘ ┴ └─────────────┘ ┴ └──────────────┘
498
499 lemma closure_eq_nhds {s : set α} : closure s = {a | 𝓝 a ⊓ principal s ≠ ⊥} :=
id └─┘ ┴ └─────┘ ┴ ┴ ┴┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴
src └─┘ └─────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴
typ └─┘ ┴ └─────┘ ┴ ┴ ┴┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴
doc └─────┘ ┴ └───────┘
500 calc closure s = - interior (- s) : closure_eq_compl_interior_compl
id └─────┘ ┴ ┴ └──────┘ ┴ ┴ └─────────────────────────────┘
src └─────┘ ┴ └──────┘ ┴ └─────────────────────────────┘
typ └─────┘ ┴ ┴ └──────┘ ┴ ┴ └─────────────────────────────┘
doc └─────┘ └──────┘
501 ... = {a | ¬ 𝓝 a ≤ principal (-s)} : by rw [interior_eq_nhds]; refl
id ┴┴ ┴ ┴ ┴ ┴ └───────┘ ┴┴ └──────────────┘
src ┴ ┴ ┴ ┴ └───────┘ ┴ └──┘└──────────────┘┴ └────
typ ┴┴ ┴ ┴ ┴ ┴ └───────┘ ┴┴ └──┘└──────────────┘┴ └────
doc ┴ └───────┘ └──┘ ┴ └────
txt └──┘ ┴ └────
par └──┘ ┴ └────
pid └┘ ┴ └
st └───────────────────┘┴└──────
502 ... = {a | 𝓝 a ⊓ principal s ≠ ⊥} : set.ext $ assume a, not_congr
id ┴┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └─────┘ ┴ └───────┘
src ─┘ ┴ ┴ ┴ └───────┘ ┴ ┴ └─────┘ └───────┘
typ ─┘ ┴┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └─────┘ ┴ └───────┘
doc ─┘ ┴ └───────┘
txt ─┘
par ─┘
pid ─┘
st ─┘
503 (inf_eq_bot_iff_le_compl
id └─────────────────────┘
src └─────────────────────┘
typ └─────────────────────┘
504 (show principal s ⊔ principal (-s) = ⊤, by simp only [sup_principal, union_compl_self, principal_univ])
id └───────┘ ┴ ┴ └───────┘ ┴┴ ┴ ┴ └───────────┘ └──────────────┘ └────────────┘
src └───────┘ ┴ └───────┘ ┴ ┴ ┴ └─────────┘└───────────┘└┘└──────────────┘└┘└────────────┘┴
typ └───────┘ ┴ ┴ └───────┘ ┴┴ ┴ ┴ └─────────┘└───────────┘└┘└──────────────┘└┘└────────────┘┴
doc └───────┘ └───────┘ └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st └──────────────────────────────────────────────────────────┘
505 (by simp only [inf_principal, inter_compl_self, principal_empty])).symm
id └───────────┘ └──────────────┘ └─────────────┘ └──┘
src └─────────┘└───────────┘└┘└──────────────┘└┘└─────────────┘┴ └──┘
typ └─────────┘└───────────┘└┘└──────────────┘└┘└─────────────┘┴ └──┘
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st └───────────────────────────────────────────────────────────┘
506
507 theorem mem_closure_iff_nhds {s : set α} {a : α} :
id └─┘ ┴ ┴
src └─┘
typ └─┘ ┴ ┴
508 a ∈ closure s ↔ ∀ t ∈ 𝓝 a, (t ∩ s).nonempty :=
id ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘
src ┴ └─────┘ ┴ ┴ ┴ └──────┘
typ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘
doc └─────┘ ┴ └──────┘
509 mem_closure_iff.trans
id └─────────────┘└────┘
src └─────────────┘└────┘
typ └─────────────┘└────┘
510 ⟨λ H t ht, nonempty.mono
id ┴ ┴ └┘ └───────────┘
src └───────────┘
typ ┴ ┴ └┘ └───────────┘
511 (inter_subset_inter_left _ interior_subset)
id └─────────────────────┘ └─────────────┘
src └─────────────────────┘ └─────────────┘
typ └─────────────────────┘ └─────────────┘
512 (H _ is_open_interior (mem_interior_iff_mem_nhds.2 ht)),
id ┴ └──────────────┘ └───────────────────────┘┴ └┘
src └──────────────┘ └───────────────────────┘┴
typ ┴ └──────────────┘ └───────────────────────┘┴ └┘
513 λ H o oo ao, H _ (mem_nhds_sets oo ao)⟩
id ┴ ┴ └┘ └┘ ┴ └───────────┘ └┘ └┘
src └───────────┘
typ ┴ ┴ └┘ └┘ ┴ └───────────┘ └┘ └┘
514
515 /-- `x` belongs to the closure of `s` if and only if some ultrafilter
516 supported on `s` converges to `x`. -/
517 lemma mem_closure_iff_ultrafilter {s : set α} {x : α} :
id └─┘ ┴ ┴
src └─┘
typ └─┘ ┴ ┴
518 x ∈ closure s ↔ ∃ (u : ultrafilter α), s ∈ u.val ∧ u.val ≤ 𝓝 x :=
id ┴ ┴ └─────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴└──┘ ┴ ┴ ┴
src ┴ └─────┘ ┴ ┴ └─────────┘ ┴ ┴ └──┘ ┴ └──┘ ┴ ┴
typ ┴ ┴ └─────┘ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴└──┘ ┴ ┴ ┴
doc └─────┘ └─────────┘ ┴
519 begin
st └─────
520 rw closure_eq_nhds, change 𝓝 x ⊓ principal s ≠ ⊥ ↔ _, symmetry,
id └─────────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴
src └─┘└─────────────┘ └─────┘┴┴ ┴┴┴└───────┘┴ ┴┴┴┴┴ └┘ └──────┘
typ └─┘└─────────────┘ └─────┘┴┴┴┴┴┴└───────┘┴┴┴┴┴┴┴ └┘ └──────┘
doc └─┘ └─────┘┴┴ ┴ ┴└───────┘┴ ┴ ┴ ┴ └┘ └──────┘
txt └─┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └──────┘
par └─┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └──────┘
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
st ───────────────────┘└────────────────────────────────┘└────────┘└─
521 convert exists_ultrafilter_iff _, ext u,
id └────────────────────┘
src └──────┘└────────────────────┘└┘ └───┘
typ └──────┘└────────────────────┘└┘ └───┘
doc └──────┘ └┘ └───┘
txt └──────┘ └┘ └───┘
par └──────┘ └┘ └───┘
pid ┴ └┘ └┘
st ─────────────────────────────────┘└─────┘└─
522 rw [←le_principal_iff, inf_comm, le_inf_iff]
id └──────────────┘ └──────┘ └────────┘
src └───┘└──────────────┘└┘└──────┘└┘└────────┘└┘
typ └───┘└──────────────┘└┘└──────┘└┘└────────┘└┘
doc └───┘ └┘ └┘ └┘
txt └───┘ └┘ └┘ └┘
par └───┘ └┘ └┘ └┘
pid └─┘ └┘ └┘ ┴┴
st ──────────────────────┘└────────┘└──────────┘┴┴
523 end
st └─┘
524
525 lemma is_closed_iff_nhds {s : set α} : is_closed s ↔ ∀a, 𝓝 a ⊓ principal s ≠ ⊥ → a ∈ s :=
id └─┘ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └───────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴
typ └─┘ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────┘ ┴ └───────┘
526 calc is_closed s ↔ closure s = s : by rw [closure_eq_iff_is_closed]
id └───────┘ ┴ └─────┘ ┴ ┴ ┴ └──────────────────────┘
src └───────┘ └─────┘ ┴ └──┘└──────────────────────┘└─
typ └───────┘ ┴ └─────┘ ┴ ┴ ┴ └──┘└──────────────────────┘└─
doc └───────┘ └─────┘ └──┘ └─
txt └──┘ └─
par └──┘ └─
pid └┘ ┴└
st └───────────────────────────┘┴└
527 ... ↔ closure s ⊆ s : ⟨assume h, by rw h, assume h, subset.antisymm h subset_closure⟩
id └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────┘ ┴ └────────────┘
src ─┘ └─────┘ ┴ └─┘ └─────────────┘ └────────────┘
typ ─┘ └─────┘ ┴ ┴ ┴ ┴ └─┘┴ ┴ └─────────────┘ ┴ └────────────┘
doc ─┘ └─────┘ └─┘
txt ─┘ └─┘
par ─┘ └─┘
pid ─┘ ┴
st ─┘ └───┘
528 ... ↔ (∀a, 𝓝 a ⊓ principal s ≠ ⊥ → a ∈ s) : by rw [closure_eq_nhds]; refl
id ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────────────┘
src ┴ ┴ └───────┘ ┴ ┴ ┴ └──┘└─────────────┘┴ └────
typ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘└─────────────┘┴ └────
doc ┴ └───────┘ └──┘ ┴ └────
txt └──┘ ┴ └────
par └──┘ ┴ └────
pid └┘ ┴ └
st └──────────────────┘┴└──────
529
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
530 lemma closure_inter_open {s t : set α} (h : is_open s) : s ∩ closure t ⊆ closure (s ∩ t) :=
id └─┘ ┴ └─────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴
src └─┘ └─────┘ ┴ └─────┘ ┴ └─────┘ ┴
typ └─┘ ┴ └─────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴
doc └─────┘ └─────┘ └─────┘
531 assume a ⟨hs, ht⟩,
id ┴ ┴└┘
typ ┴ ┴└┘
532 have s ∈ 𝓝 a, from mem_nhds_sets h hs,
id ┴ ┴ ┴ ┴ └───────────┘ ┴
src ┴ ┴ └───────────┘
typ ┴ ┴ ┴ ┴ └───────────┘ ┴
doc ┴
533 have 𝓝 a ⊓ principal s = 𝓝 a, from inf_of_le_left $ by rwa le_principal_iff,
id ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ └────────────┘ └──────────────┘
src ┴ ┴ └───────┘ ┴ ┴ └────────────┘ └──┘└──────────────┘
typ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ └────────────┘ └──┘└──────────────┘
doc ┴ └───────┘ ┴ └──┘
txt └──┘
par └──┘
pid ┴
st └───────────────────┘
534 have 𝓝 a ⊓ principal (s ∩ t) ≠ ⊥,
id ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └───────┘ ┴ ┴ ┴
typ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴
doc ┴ └───────┘
535 from calc 𝓝 a ⊓ principal (s ∩ t) = 𝓝 a ⊓ (principal s ⊓ principal t) : by rw inf_principal
id ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └───────┘ ┴ └───────────┘
src ┴ ┴ └───────┘ ┴ ┴ ┴ └───────┘ ┴ └───────┘ └─┘└───────────┘└
typ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └───────┘ ┴ └─┘└───────────┘└
doc ┴ └───────┘ ┴ └───────┘ └───────┘ └─┘ └
txt └─┘ └
par └─┘ └
pid ┴ └
st └─────────────────
536 ... = 𝓝 a ⊓ principal t : by rw [←inf_assoc, this]
id ┴ ┴ ┴ └───────┘ ┴ └───────┘ └──┘
src ───┘ ┴ ┴ └───────┘ └───┘└───────┘└┘ └─
typ ───┘ ┴ ┴ ┴ └───────┘ ┴ └───┘└───────┘└┘└──┘└─
doc ───┘ ┴ └───────┘ └───┘ └┘ └─
txt ───┘ └───┘ └┘ └─
par ───┘ └───┘ └┘ └─
pid ───┘ └─┘ └┘ ┴└
st ───┘ └─────────────┘└────┘┴└
537 ... ≠ ⊥ : by rw [closure_eq_nhds] at ht; assumption,
id ┴ └─────────────┘
src ───┘ ┴ └──┘└─────────────┘└─────┘ └────────┘
typ ───┘ ┴ └──┘└─────────────┘└─────┘ └────────┘
doc ───┘ └──┘ └─────┘ └────────┘
txt ───┘ └──┘ └─────┘ └────────┘
par ───┘ └──┘ └─────┘ └────────┘
pid ───┘ └┘ ┴└────┘
st ───┘ └──────────────────┘┴└────────────────┘
538 by rw [closure_eq_nhds]; assumption
id └─────────────┘
src └──┘└─────────────┘┴ └──────────
typ └──┘└─────────────┘┴ └──────────
doc └──┘ ┴ └──────────
txt └──┘ ┴ └──────────
par └──┘ ┴ └──────────
pid └┘ ┴ └
st └──────────────────┘┴└────────────
539
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
540 lemma closure_diff {s t : set α} : closure s - closure t ⊆ closure (s - t) :=
id └─┘ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴
src └─┘ └─────┘ ┴ └─────┘ ┴ └─────┘ ┴
typ └─┘ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴
doc └─────┘ └─────┘ └─────┘
541 calc closure s \ closure t = (- closure t) ∩ closure s : by simp only [diff_eq, inter_comm]
id └─────┘ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴ └─────┘ └────────┘
src └─────┘ ┴ └─────┘ ┴ └─────┘ ┴ └─────┘ └─────────┘└─────┘└┘└────────┘└─
typ └─────┘ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴ └─────────┘└─────┘└┘└────────┘└─
doc └─────┘ └─────┘ └─────┘ └─────┘ └─────────┘ └┘ └─
txt └─────────┘ └┘ └─
par └─────────┘ └┘ └─
pid ┴└──┘└┘ └┘ ┴└
st └────────────────────────────────
542 ... ⊆ closure (- closure t ∩ s) : closure_inter_open $ is_open_compl_iff.mpr $ is_closed_closure
id └─────┘ ┴ └─────┘ ┴ ┴ ┴ └────────────────┘ └───────────────┘└──┘ └───────────────┘
src ─┘ └─────┘ ┴ └─────┘ ┴ └────────────────┘ └───────────────┘└──┘ └───────────────┘
typ ─┘ └─────┘ ┴ └─────┘ ┴ ┴ ┴ └────────────────┘ └───────────────┘└──┘ └───────────────┘
doc ─┘ └─────┘ └─────┘
txt ─┘
par ─┘
pid ─┘
st ─┘
543 ... = closure (s \ closure t) : by simp only [diff_eq, inter_comm]
id └─────┘ ┴ ┴ └─────┘ ┴ └─────┘ └────────┘
src └─────┘ ┴ └─────┘ └─────────┘└─────┘└┘└────────┘└─
typ └─────┘ ┴ ┴ └─────┘ ┴ └─────────┘└─────┘└┘└────────┘└─
doc └─────┘ └─────┘ └─────────┘ └┘ └─
txt └─────────┘ └┘ └─
par └─────────┘ └┘ └─
pid ┴└──┘└┘ └┘ ┴└
st └────────────────────────────────
544 ... ⊆ closure (s \ t) : closure_mono $ diff_subset_diff (subset.refl s) subset_closure
id └─────┘ ┴ ┴ ┴ └──────────┘ └──────────────┘ └─────────┘ ┴ └────────────┘
src ─┘ └─────┘ ┴ └──────────┘ └──────────────┘ └─────────┘ └────────────┘
typ ─┘ └─────┘ ┴ ┴ ┴ └──────────┘ └──────────────┘ └─────────┘ ┴ └────────────┘
doc ─┘ └─────┘
txt ─┘
par ─┘
pid ─┘
st ─┘
545
546 lemma mem_of_closed_of_tendsto {f : β → α} {b : filter β} {a : α} {s : set α}
id ┴ ┴ └────┘ ┴ ┴ └─┘ ┴
src └────┘ └─┘
typ ┴ ┴ └────┘ ┴ ┴ └─┘ ┴
547 (hb : b ≠ ⊥) (hf : tendsto f b (𝓝 a)) (hs : is_closed s) (h : f ⁻¹' s ∈ b) : a ∈ s :=
id ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └─────┘ ┴ └───────┘ └─┘ ┴ ┴
typ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ ┴ └───────┘ └─┘
548 have b.map f ≤ 𝓝 a ⊓ principal s,
id ┴└──┘ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴
src └──┘ ┴ ┴ ┴ └───────┘
typ ┴└──┘ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴
doc └──┘ ┴ └───────┘
549 from le_trans (le_inf (le_refl _) (le_principal_iff.mpr h)) (inf_le_inf hf (le_refl _)),
id └──────┘ └────┘ └─────┘ └──────────────┘└──┘ ┴ └────────┘ └┘ └─────┘
src └──────┘ └────┘ └─────┘ └──────────────┘└──┘ └────────┘ └─────┘
typ └──────┘ └────┘ └─────┘ └──────────────┘└──┘ ┴ └────────┘ └┘ └─────┘
550 is_closed_iff_nhds.mp hs a $ ne_bot_of_le_ne_bot (map_ne_bot hb) this
id └────────────────┘└─┘ └┘ ┴ └─────────────────┘ └────────┘ └┘ └──┘
src └────────────────┘└─┘ └─────────────────┘ └────────┘
typ └────────────────┘└─┘ └┘ ┴ └─────────────────┘ └────────┘ └┘ └──┘
551
552 lemma mem_of_closed_of_tendsto' {f : β → α} {x : filter β} {a : α} {s : set α}
id ┴ ┴ └────┘ ┴ ┴ └─┘ ┴
src └────┘ └─┘
typ ┴ ┴ └────┘ ┴ ┴ └─┘ ┴
553 (hf : tendsto f x (𝓝 a)) (hs : is_closed s) (h : x ⊓ principal (f ⁻¹' s) ≠ ⊥) : a ∈ s :=
id └─────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └───────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ └───────┘ ┴ └───────┘ └─┘ ┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └───────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ ┴ └───────┘ └───────┘ └─┘
554 is_closed_iff_nhds.mp hs _ $ ne_bot_of_le_ne_bot (@map_ne_bot _ _ _ f h) $
id └────────────────┘└─┘ └┘ └─────────────────┘ └────────┘ ┴ ┴
src └────────────────┘└─┘ └─────────────────┘ └────────┘
typ └────────────────┘└─┘ └┘ └─────────────────┘ └────────┘ ┴ ┴
555 le_inf (le_trans (map_mono $ inf_le_left) hf) $
id └────┘ └──────┘ └──────┘ └─────────┘ └┘
src └────┘ └──────┘ └──────┘ └─────────┘
typ └────┘ └──────┘ └──────┘ └─────────┘ └┘
556 le_trans (map_mono $ inf_le_right_of_le $ by simp only [comap_principal, le_principal_iff]; exact subset.refl _) (@map_comap_le _ _ _ f)
id └──────┘ └──────┘ └────────────────┘ └─────────────┘ └──────────────┘ └─────────┘ └──────────┘ ┴
src └──────┘ └──────┘ └────────────────┘ └─────────┘└─────────────┘└┘└──────────────┘┴ └────┘└─────────┘└┘ └──────────┘
typ └──────┘ └──────┘ └────────────────┘ └─────────┘└─────────────┘└┘└──────────────┘┴ └────┘└─────────┘└┘ └──────────┘ ┴
doc └─────────┘ └┘ ┴ └────┘ └┘
txt └─────────┘ └┘ ┴ └────┘ └┘
par └─────────┘ └┘ ┴ └────┘ └┘
pid ┴└──┘└┘ └┘ ┴ ┴ └┘
st └─────────────────────────────────────────────────────────────────┘
557
558 lemma mem_closure_of_tendsto {f : β → α} {b : filter β} {a : α} {s : set α}
id ┴ ┴ └────┘ ┴ ┴ └─┘ ┴
src └────┘ └─┘
typ ┴ ┴ └────┘ ┴ ┴ └─┘ ┴
559 (hb : b ≠ ⊥) (hf : tendsto f b (𝓝 a)) (h : f ⁻¹' s ∈ b) : a ∈ closure s :=
id ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
src ┴ ┴ └─────┘ ┴ └─┘ ┴ ┴ └─────┘
typ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
doc └─────┘ ┴ └─┘ └─────┘
560 mem_of_closed_of_tendsto hb hf (is_closed_closure) $
id └──────────────────────┘ └┘ └┘ └───────────────┘
src └──────────────────────┘ └───────────────┘
typ └──────────────────────┘ └┘ └┘ └───────────────┘
561 filter.mem_sets_of_superset h (preimage_mono subset_closure)
id └─────────────────────────┘ ┴ └───────────┘ └────────────┘
src └─────────────────────────┘ └───────────┘ └────────────┘
typ └─────────────────────────┘ ┴ └───────────┘ └────────────┘
562
563 /-- Suppose that `f` sends the complement to `s` to a single point `a`, and `l` is some filter.
564 Then `f` tends to `a` along `l` restricted to `s` if and only it tends to `a` along `l`. -/
565 lemma tendsto_inf_principal_nhds_iff_of_forall_eq {f : β → α} {l : filter β} {s : set β}
id ┴ ┴ └────┘ ┴ └─┘ ┴
src └────┘ └─┘
typ ┴ ┴ └────┘ ┴ └─┘ ┴
566 {a : α} (h : ∀ x ∉ s, f x = a) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
567 tendsto f (l ⊓ principal s) (𝓝 a) ↔ tendsto f l (𝓝 a) :=
id └─────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
src └─────┘ ┴ └───────┘ ┴ ┴ └─────┘ ┴
typ └─────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
doc └─────┘ └───────┘ ┴ └─────┘ ┴
568 begin
st └─────
569 rw [tendsto_iff_comap, tendsto_iff_comap],
id └───────────────┘ └───────────────┘
src └──┘└───────────────┘└┘└───────────────┘┴
typ └──┘└───────────────┘└┘└───────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ──────────────────────┘└─────────────────┘└──
570 replace h : principal (-s) ≤ comap f (𝓝 a),
id └───────┘ ┴┴ ┴ └───┘ ┴ ┴ ┴
src └──────────┘└───────┘┴ ┴ └┘┴┴└───┘┴ ┴ ┴┴ ┴
typ └──────────┘└───────┘┴ ┴┴└┘┴┴└───┘┴┴┴ ┴┴┴┴
doc └──────────┘└───────┘┴ └┘ ┴└───┘┴ ┴ ┴┴ ┴
txt └──────────┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴
par └──────────┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴
pid └┘└─┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────┘└─
571 { rintros U ⟨t, ht, htU⟩ x hx,
src └─────────────────────────┘
typ └─────────────────────────┘
doc └─────────────────────────┘
txt └─────────────────────────┘
par └─────────────────────────┘
pid └──────────────────┘
st ───┘└─────────────────────────┘└─
572 have : f x ∈ t, from (h x hx).symm ▸ mem_of_nhds ht,
id ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─────────┘ └┘
src └─────┘ ┴ ┴┴┴ └───┘ ┴ ┴ └─────┘┴┴└─────────┘┴
typ └─────┘┴┴┴┴┴┴┴ └───┘ ┴┴┴┴└┘└─────┘┴┴└─────────┘┴└┘
doc └─────┘ ┴ ┴ ┴ └───┘ ┴ ┴ └─────┘ ┴ ┴
txt └─────┘ ┴ ┴ ┴ └───┘ ┴ ┴ └─────┘ ┴ ┴
par └─────┘ ┴ ┴ ┴ └───┘ ┴ ┴ └─────┘ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴ └───┘ ┴ ┴ └─────┘ ┴ ┴
st ─────────────────┘└───────────────────────────────────┘└─
573 exact htU this },
id └─┘ └──┘
src └────┘ ┴ ┴
typ └────┘└─┘┴└──┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ──────────────────┘└┘└
574 refine ⟨λ h', _, le_trans inf_le_left⟩,
id └──────┘ └─────────┘
src └─────┘ └──────┘└──────┘┴└─────────┘┴
typ └─────┘ └──────┘└──────┘┴└─────────┘┴
doc └─────┘ └──────┘ ┴ ┴
txt └─────┘ └──────┘ ┴ ┴
par └─────┘ └──────┘ ┴ ┴
pid ┴ └──────┘ ┴ ┴
st ───────────────────────────────────────┘└─
575 have := sup_le h' h,
id └────┘ └┘ ┴
src └──────┘└────┘┴ ┴
typ └──────┘└────┘┴└┘┴┴
doc └──────┘ ┴ ┴
txt └──────┘ ┴ ┴
par └──────┘ ┴ ┴
pid └───┘└─┘ ┴ ┴
st ────────────────────┘└─
576 rw [sup_inf_right, sup_principal, union_compl_self, principal_univ,
id └───────────┘ └───────────┘ └──────────────┘ └────────────┘
src └──┘└───────────┘└┘└───────────┘└┘└──────────────┘└┘└────────────┘└─
typ └──┘└───────────┘└┘└───────────┘└┘└──────────────┘└┘└────────────┘└─
doc └──┘ └┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └┘ └─
par └──┘ └┘ └┘ └┘ └─
pid └┘ └┘ └┘ └┘ └─
st ──────────────────┘└─────────────┘└────────────────┘└──────────────┘└─
577 inf_top_eq, sup_le_iff] at this,
id └────────┘ └────────┘
src ───┘└────────┘└┘└────────┘└───────┘
typ ───┘└────────┘└┘└────────┘└───────┘
doc ───┘ └┘ └───────┘
txt ───┘ └┘ └───────┘
par ───┘ └┘ └───────┘
pid ───┘ └┘ ┴└──────┘
st ─────────────┘└──────────┘┴└──────┘└─
578 exact this.1
id └──┘
src └────┘ └─┘
typ └────┘└──┘└─┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └─┘
st ──────────────┘
579 end
st └─┘
580
581 section lim
582 variables [inhabited α]
id └───────┘
src └───────┘
typ └───────┘
583
584 /-- If `f` is a filter, then `lim f` is a limit of the filter, if it exists. -/
585 noncomputable def lim (f : filter α) : α := epsilon $ λa, f ≤ 𝓝 a
id └────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴
src └────┘ └─────┘ ┴ ┴
typ └────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴
doc ┴
586
587 lemma lim_spec {f : filter α} (h : ∃a, f ≤ 𝓝 a) : f ≤ 𝓝 (lim f) := epsilon_spec h
id └────┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └──────────┘ ┴
src └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──────────┘
typ └────┘ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └──────────┘ ┴
doc ┴ ┴ └─┘
588 end lim
589
590
591 /- locally finite family [General Topology (Bourbaki, 1995)] -/
592 section locally_finite
593
594 /-- A family of sets in `set α` is locally finite if at every point `x:α`,
595 there is a neighborhood of `x` which meets only finitely many sets in the family -/
596 def locally_finite (f : β → set α) :=
id ┴ └─┘ ┴
src └─┘
typ ┴ └─┘ ┴
597 ∀x:α, ∃t ∈ 𝓝 x, finite {i | (f i ∩ t).nonempty }
id ┴ ┴┴ ┴ ┴┴ └────┘ ┴┴ ┴ ┴ ┴ ┴ └──────┘
src ┴ ┴ ┴ └────┘ ┴ ┴ └──────┘
typ ┴ ┴┴ ┴ ┴┴ └────┘ ┴┴ ┴ ┴ ┴ ┴ └──────┘
doc ┴ └────┘ └──────┘
598
599 lemma locally_finite_of_finite {f : β → set α} (h : finite (univ : set β)) : locally_finite f :=
id ┴ └─┘ ┴ └────┘ └──┘ └─┘ ┴ └────────────┘ ┴
src └─┘ └────┘ └──┘ └─┘ └────────────┘
typ ┴ └─┘ ┴ └────┘ └──┘ └─┘ ┴ └────────────┘ ┴
doc └────┘ └────────────┘
600 assume x, ⟨univ, univ_mem_sets, finite_subset h $ subset_univ _⟩
id ┴ └──┘ └───────────┘ └───────────┘ ┴ └─────────┘
src └──┘ └───────────┘ └───────────┘ └─────────┘
typ ┴ └──┘ └───────────┘ └───────────┘ ┴ └─────────┘
601
602 lemma locally_finite_subset
603 {f₁ f₂ : β → set α} (hf₂ : locally_finite f₂) (hf : ∀b, f₁ b ⊆ f₂ b) : locally_finite f₁ :=
id ┴ └─┘ ┴ └────────────┘ └┘ ┴ └┘ ┴ ┴ └┘ ┴ └────────────┘ └┘
src └─┘ └────────────┘ ┴ └────────────┘
typ ┴ └─┘ ┴ └────────────┘ └┘ ┴ └┘ ┴ ┴ └┘ ┴ └────────────┘ └┘
doc └────────────┘ └────────────┘
604 assume a,
id ┴
typ ┴
605 let ⟨t, ht₁, ht₂⟩ := hf₂ a in
id └─┘ ┴ └─┘ └─┘ └─┘ ┴
typ └─┘ ┴ └─┘ └─┘ └─┘ ┴
606 ⟨t, ht₁, finite_subset ht₂ $ assume i hi,
id └───────────┘ ┴ └┘
src └───────────┘
typ └───────────┘ ┴ └┘
607 hi.mono $ inter_subset_inter (hf i) $ subset.refl _⟩
id └┘└───┘ └────────────────┘ └┘ ┴ └─────────┘
src └───┘ └────────────────┘ └─────────┘
typ └┘└───┘ └────────────────┘ └┘ ┴ └─────────┘
608
609 lemma is_closed_Union_of_locally_finite {f : β → set α}
id ┴ └─┘ ┴
src └─┘
typ ┴ └─┘ ┴
610 (h₁ : locally_finite f) (h₂ : ∀i, is_closed (f i)) : is_closed (⋃i, f i) :=
id └────────────┘ ┴ ┴ └───────┘ ┴ ┴ └───────┘ ┴┴┴ ┴ ┴
src └────────────┘ └───────┘ └───────┘ ┴ ┴
typ └────────────┘ ┴ ┴ └───────┘ ┴ ┴ └───────┘ ┴┴┴ ┴ ┴
doc └────────────┘ └───────┘ └───────┘ ┴ ┴
611 is_open_iff_nhds.mpr $ assume a, assume h : a ∉ (⋃i, f i),
id └──────────────┘└──┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴
src └──────────────┘└──┘ ┴ ┴ ┴
typ └──────────────┘└──┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴
doc ┴ ┴
612 have ∀i, a ∈ -f i,
id ┴ ┴ ┴ ┴┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴┴ ┴
613 from assume i hi, h $ mem_Union.2 ⟨i, hi⟩,
id ┴ └┘ ┴ └───────┘┴ ┴ └┘
src └───────┘┴
typ ┴ └┘ ┴ └───────┘┴ ┴ └┘
614 have ∀i, - f i ∈ (𝓝 a).sets,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
src ┴ ┴ ┴ └──┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
doc ┴
615 by rw [nhds_sets]; exact assume i, ⟨- f i, subset.refl _, h₂ i, this i⟩,
id └───────┘ ┴ ┴ └─────────┘ └┘ └──┘
src └──┘└───────┘┴ └────┘ └──┘ ┴┴ ┴ └┘└─────────┘└──┘ ┴ └┘ ┴ ┴
typ └──┘└───────┘┴ └────┘ └──┘ ┴┴┴┴ └┘└─────────┘└──┘└┘┴ └┘└──┘┴ ┴
doc └──┘ ┴ └────┘ └──┘ ┴ ┴ └┘ └──┘ ┴ └┘ ┴ ┴
txt └──┘ ┴ └────┘ └──┘ ┴ ┴ └┘ └──┘ ┴ └┘ ┴ ┴
par └──┘ ┴ └────┘ └──┘ ┴ ┴ └┘ └──┘ ┴ └┘ ┴ ┴
pid └┘ ┴ ┴ └──┘ ┴ ┴ └┘ └──┘ ┴ └┘ ┴ ┴
st └────────────┘┴└────────────────────────────────────────────────────┘
616 let ⟨t, h_sets, (h_fin : finite {i | (f i ∩ t).nonempty })⟩ := h₁ a in
id └─┘ ┴ └────┘ ┴┴ ┴ ┴ ┴ └──────┘ └┘ ┴
src └────┘ ┴ ┴ └──────┘
typ └─┘ ┴ └────┘ ┴┴ ┴ ┴ ┴ └──────┘ └┘ ┴
doc └────┘ └──────┘
617
618 calc 𝓝 a ≤ principal (t ∩ (⋂ i∈{i | (f i ∩ t).nonempty }, - f i)) :
id ┴ ┴ └───────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
src ┴ └───────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴
typ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
doc ┴ └───────┘ ┴ └──────┘ ┴
619 begin
st └─────
620 rw [le_principal_iff],
id └──────────────┘
src └──┘└──────────────┘┴
typ └──┘└──────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ───────────────────────┘└──
621 apply @filter.inter_mem_sets _ (𝓝 a) _ _ h_sets,
id └───────────────────┘ ┴ ┴ └────┘
src └────┘ └───────────────────┘└─┘ ┴┴ └────┘
typ └────┘ └───────────────────┘└─┘ ┴┴┴└────┘└────┘
doc └────┘ └─┘ ┴┴ └────┘
txt └────┘ └─┘ ┴ └────┘
par └────┘ └─┘ ┴ └────┘
pid ┴ └─┘ ┴ └────┘
st ──────────────────────────────────────────────────┘└─
622 apply @filter.Inter_mem_sets _ (𝓝 a) _ _ _ h_fin,
id └───────────────────┘ ┴ └───┘
src └────┘ └───────────────────┘└─┘ ┴ └──────┘
typ └────┘ └───────────────────┘└─┘ ┴┴└──────┘└───┘
doc └────┘ └─┘ ┴ └──────┘
txt └────┘ └─┘ ┴ └──────┘
par └────┘ └─┘ ┴ └──────┘
pid ┴ └─┘ ┴ └──────┘
st ───────────────────────────────────────────────────┘└─
623 exact assume i h, this i
id └──┘
src └────┘ └────┘ ┴ └
typ └────┘ └────┘└──┘┴ └
doc └────┘ └────┘ ┴ └
txt └────┘ └────┘ ┴ └
par └────┘ └────┘ ┴ └
pid ┴ └────┘ ┴ └
st ─────────────────────────────
624 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
625 ... ≤ principal (- ⋃i, f i) :
id └───────┘ ┴ ┴┴┴ ┴ ┴
src └───────┘ ┴ ┴ ┴
typ └───────┘ ┴ ┴┴┴ ┴ ┴
doc └───────┘ ┴ ┴
626 begin
st └─────
627 simp only [principal_mono, subset_def, mem_compl_eq, mem_inter_eq,
id └────────────┘ └────────┘ └──────────┘ └──────────┘
src └─────────┘└────────────┘└┘└────────┘└┘└──────────┘└┘└──────────┘└─
typ └─────────┘└────────────┘└┘└────────┘└┘└──────────┘└┘└──────────┘└─
doc └─────────┘ └┘ └┘ └┘ └─
txt └─────────┘ └┘ └┘ └┘ └─
par └─────────┘ └┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ └┘ └─
st ───────────────────────────────────────────────────────────────────────
628 mem_Inter, mem_set_of_eq, mem_Union, and_imp, not_exists,
id └───────┘ └───────────┘ └───────┘ └─────┘ └────────┘
src ─────┘└───────┘└┘└───────────┘└┘└───────┘└┘└─────┘└┘└────────┘└─
typ ─────┘└───────┘└┘└───────────┘└┘└───────┘└┘└─────┘└┘└────────┘└─
doc ─────┘ └┘ └┘ └┘ └┘ └─
txt ─────┘ └┘ └┘ └┘ └┘ └─
par ─────┘ └┘ └┘ └┘ └┘ └─
pid ─────┘ └┘ └┘ └┘ └┘ └─
st ────────────────────────────────────────────────────────────────
629 exists_imp_distrib, ne_empty_iff_nonempty, set.nonempty],
id └────────────────┘ └───────────────────┘ └──────────┘
src ─────┘└────────────────┘└┘└───────────────────┘└┘└──────────┘┴
typ ─────┘└────────────────┘└┘└───────────────────┘└┘└──────────┘┴
doc ─────┘ └┘ └┘└──────────┘┴
txt ─────┘ └┘ └┘ ┴
par ─────┘ └┘ └┘ ┴
pid ─────┘ └┘ └┘ ┴
st ─────────────────────────────────────────────────────────────┘└─
630 exact assume x xt ht i xfi, ht i x xfi xt xfi
src └────┘ └──────────────┘ ┴ ┴ ┴ ┴ ┴ └
typ └────┘ └──────────────┘ ┴ ┴ ┴ ┴ ┴ └
doc └────┘ └──────────────┘ ┴ ┴ ┴ ┴ ┴ └
txt └────┘ └──────────────┘ ┴ ┴ ┴ ┴ ┴ └
par └────┘ └──────────────┘ ┴ ┴ ┴ ┴ ┴ └
pid ┴ └──────────────┘ ┴ ┴ ┴ ┴ ┴ └
st ──────────────────────────────────────────────────
631 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
632
633 end locally_finite
634
635 end topological_space
636
637 section continuous
638 variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
id ┴
typ ┴
639 variables [topological_space α] [topological_space β] [topological_space γ]
id └───────────────┘ └───────────────┘ └───────────────┘
src └───────────────┘ └───────────────┘ └───────────────┘
typ └───────────────┘ └───────────────┘ └───────────────┘
doc └───────────────┘ └───────────────┘ └───────────────┘
640 open_locale topological_space
641
642 /-- A function between topological spaces is continuous if the preimage
643 of every open set is open. -/
644 def continuous (f : α → β) := ∀s, is_open s → is_open (f ⁻¹' s)
id ┴ ┴ ┴ └─────┘ ┴ └─────┘ ┴ └─┘ ┴
src └─────┘ └─────┘ └─┘
typ ┴ ┴ ┴ └─────┘ ┴ └─────┘ ┴ └─┘ ┴
doc └─────┘ └─────┘ └─┘
645
646 /-- A function between topological spaces is continuous at a point `x₀`
647 if `f x` tends to `f x₀` when `x` tends to `x₀`. -/
648 def continuous_at (f : α → β) (x : α) := tendsto f (𝓝 x) (𝓝 (f x))
id ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴
typ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ ┴ ┴
649
650 lemma continuous_at.preimage_mem_nhds {f : α → β} {x : α} {t : set β} (h : continuous_at f x)
id ┴ ┴ ┴ └─┘ ┴ └───────────┘ ┴ ┴
src └─┘ └───────────┘
typ ┴ ┴ ┴ └─┘ ┴ └───────────┘ ┴ ┴
doc └───────────┘
651 (ht : t ∈ 𝓝 (f x)) : f ⁻¹' t ∈ 𝓝 x :=
id ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src ┴ ┴ └─┘ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
doc ┴ └─┘ ┴
652 h ht
id ┴ └┘
typ ┴ └┘
653
654 lemma continuous_id : continuous (id : α → α) :=
id └────────┘ └┘ ┴ ┴
src └────────┘ └┘
typ └────────┘ └┘ ┴ ┴
doc └────────┘
655 assume s h, h
id ┴ ┴ ┴
typ ┴ ┴ ┴
656
657 lemma continuous.comp {g : β → γ} {f : α → β} (hg : continuous g) (hf : continuous f) :
id ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴
src └────────┘ └────────┘
typ ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴
doc └────────┘ └────────┘
658 continuous (g ∘ f) :=
id └────────┘ ┴ ┴ ┴
src └────────┘ ┴
typ └────────┘ ┴ ┴ ┴
doc └────────┘
659 assume s h, hf _ (hg s h)
id ┴ ┴ └┘ └┘ ┴ ┴
typ ┴ ┴ └┘ └┘ ┴ ┴
660
661 lemma continuous_at.comp {g : β → γ} {f : α → β} {x : α}
id ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
662 (hg : continuous_at g (f x)) (hf : continuous_at f x) :
id └───────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴
src └───────────┘ └───────────┘
typ └───────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴
doc └───────────┘ └───────────┘
663 continuous_at (g ∘ f) x :=
id └───────────┘ ┴ ┴ ┴ ┴
src └───────────┘ ┴
typ └───────────┘ ┴ ┴ ┴ ┴
doc └───────────┘
664 hg.comp hf
id └┘└───┘ └┘
src └───┘
typ └┘└───┘ └┘
665
666 lemma continuous.tendsto {f : α → β} (hf : continuous f) (x) :
id ┴ ┴ └────────┘ ┴
src └────────┘
typ ┴ ┴ └────────┘ ┴
doc └────────┘
667 tendsto f (𝓝 x) (𝓝 (f x)) | s :=
id └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ ┴ ┴
668 show s ∈ 𝓝 (f x) → s ∈ map f (𝓝 x),
id ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
src ┴ ┴ ┴ └─┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
doc ┴ └─┘ ┴
669 by simp [nhds_sets]; exact
id └───────┘
src └────┘└───────┘┴ └────┘
typ └────┘└───────┘┴ └────┘
doc └────┘ ┴ └────┘
txt └────┘ ┴ └────┘
par └────┘ ┴ └────┘
pid ┴┴ ┴ ┴
st └────────────────────────
670 assume t t_subset t_open fx_in_t,
src └───────────────────────────
typ └───────────────────────────
doc └───────────────────────────
txt └───────────────────────────
par └───────────────────────────
pid └───────────────────────────
st ──────────────────────────────────
671 ⟨f ⁻¹' t, preimage_mono t_subset, hf t t_open, fx_in_t⟩
id ┴ └─┘ └───────────┘ └┘
src ─┘ ┴└─┘┴ └┘└───────────┘┴ └┘ ┴ ┴ └┘ └─
typ ─┘ ┴┴└─┘┴ └┘└───────────┘┴ └┘└┘┴ ┴ └┘ └─
doc ─┘ ┴└─┘┴ └┘ ┴ └┘ ┴ ┴ └┘ └─
txt ─┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ └─
par ─┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ └─
pid ─┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴└
st ──────────────────────────────────────────────────────────
672
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
673 lemma continuous.continuous_at {f : α → β} {x : α} (h : continuous f) :
id ┴ ┴ ┴ └────────┘ ┴
src └────────┘
typ ┴ ┴ ┴ └────────┘ ┴
doc └────────┘
674 continuous_at f x :=
id └───────────┘ ┴ ┴
src └───────────┘
typ └───────────┘ ┴ ┴
doc └───────────┘
675 h.tendsto x
id ┴└──────┘ ┴
src └──────┘
typ ┴└──────┘ ┴
676
677 lemma continuous_iff_continuous_at {f : α → β} : continuous f ↔ ∀ x, continuous_at f x :=
id ┴ ┴ └────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴
src └────────┘ ┴ └───────────┘
typ ┴ ┴ └────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴
doc └────────┘ └───────────┘
678 ⟨continuous.tendsto,
id └────────────────┘
src └────────────────┘
typ └────────────────┘
679 assume hf : ∀x, tendsto f (𝓝 x) (𝓝 (f x)),
id ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴
typ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ ┴ ┴
680 assume s, assume hs : is_open s,
id ┴ └─────┘ ┴
src └─────┘
typ ┴ └─────┘ ┴
doc └─────┘
681 have ∀a, f a ∈ s → s ∈ 𝓝 (f a),
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
682 by simp [nhds_sets]; exact assume a ha, ⟨s, subset.refl s, hs, ha⟩,
id └───────┘ └─────────┘ ┴ └┘
src └────┘└───────┘┴ └────┘ └─────┘ └┘└─────────┘┴ └┘ └┘ ┴
typ └────┘└───────┘┴ └────┘ └─────┘ └┘└─────────┘┴┴└┘└┘└┘ ┴
doc └────┘ ┴ └────┘ └─────┘ └┘ ┴ └┘ └┘ ┴
txt └────┘ ┴ └────┘ └─────┘ └┘ ┴ └┘ └┘ ┴
par └────┘ ┴ └────┘ └─────┘ └┘ ┴ └┘ └┘ ┴
pid ┴┴ ┴ ┴ └─────┘ └┘ ┴ └┘ └┘ ┴
st └──────────────────────────────────────────────────────────────┘
683 show is_open (f ⁻¹' s),
id └─────┘ ┴ └─┘ ┴
src └─────┘ └─┘
typ └─────┘ ┴ └─┘ ┴
doc └─────┘ └─┘
684 by simp [is_open_iff_nhds]; exact assume a ha, hf a (this a ha)⟩
id └──────────────┘ └┘ └──┘
src └────┘└──────────────┘┴ └────┘ └─────┘ ┴ ┴ ┴ ┴ ┴
typ └────┘└──────────────┘┴ └────┘ └─────┘└┘┴ ┴ └──┘┴ ┴ ┴
doc └────┘ ┴ └────┘ └─────┘ ┴ ┴ ┴ ┴ ┴
txt └────┘ ┴ └────┘ └─────┘ ┴ ┴ ┴ ┴ ┴
par └────┘ ┴ └────┘ └─────┘ ┴ ┴ ┴ ┴ ┴
pid ┴┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴
st └───────────────────────────────────────────────────────────┘
685
686 lemma continuous_const {b : β} : continuous (λa:α, b) :=
id ┴ └────────┘ ┴ ┴
src └────────┘
typ ┴ └────────┘ ┴ ┴
doc └────────┘
687 continuous_iff_continuous_at.mpr $ assume a, tendsto_const_nhds
id └──────────────────────────┘└──┘ ┴ └────────────────┘
src └──────────────────────────┘└──┘ └────────────────┘
typ └──────────────────────────┘└──┘ ┴ └────────────────┘
688
689 lemma continuous_at_const {x : α} {b : β} : continuous_at (λ a:α, b) x :=
id ┴ ┴ └───────────┘ ┴ ┴ ┴
src └───────────┘
typ ┴ ┴ └───────────┘ ┴ ┴ ┴
doc └───────────┘
690 continuous_const.continuous_at
id └──────────────┘└────────────┘
src └──────────────┘└────────────┘
typ └──────────────┘└────────────┘
691
692 lemma continuous_at_id {x : α} : continuous_at id x :=
id ┴ └───────────┘ └┘ ┴
src └───────────┘ └┘
typ ┴ └───────────┘ └┘ ┴
doc └───────────┘
693 continuous_id.continuous_at
id └───────────┘└────────────┘
src └───────────┘└────────────┘
typ └───────────┘└────────────┘
694
695 lemma continuous_iff_is_closed {f : α → β} :
id ┴ ┴
typ ┴ ┴
696 continuous f ↔ (∀s, is_closed s → is_closed (f ⁻¹' s)) :=
id └────────┘ ┴ ┴ ┴ └───────┘ ┴ └───────┘ ┴ └─┘ ┴
src └────────┘ ┴ └───────┘ └───────┘ └─┘
typ └────────┘ ┴ ┴ ┴ └───────┘ ┴ └───────┘ ┴ └─┘ ┴
doc └────────┘ └───────┘ └───────┘ └─┘
697 ⟨assume hf s hs, hf (-s) hs,
id └┘ ┴ └┘ └┘ ┴┴ └┘
src ┴
typ └┘ ┴ └┘ └┘ ┴┴ └┘
698 assume hf s, by rw [←is_closed_compl_iff, ←is_closed_compl_iff]; exact hf _⟩
id └┘ ┴ └─────────────────┘ └─────────────────┘ └┘
src └───┘└─────────────────┘└─┘└─────────────────┘┴ └────┘ └┘
typ └┘ ┴ └───┘└─────────────────┘└─┘└─────────────────┘┴ └────┘└┘└┘
doc └───┘ └─┘ ┴ └────┘ └┘
txt └───┘ └─┘ ┴ └────┘ └┘
par └───┘ └─┘ ┴ └────┘ └┘
pid └─┘ └─┘ ┴ ┴ └┘
st └───────────────────────┘└────────────────────┘┴└──────────┘
699
700 lemma continuous_at_iff_ultrafilter {f : α → β} (x) : continuous_at f x ↔
id ┴ ┴ └───────────┘ ┴ ┴ ┴
src └───────────┘ ┴
typ ┴ ┴ └───────────┘ ┴ ┴ ┴
doc └───────────┘
701 ∀ g, is_ultrafilter g → g ≤ 𝓝 x → g.map f ≤ 𝓝 (f x) :=
id ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴
src └────────────┘ ┴ ┴ └──┘ ┴ ┴
typ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴
doc └────────────┘ ┴ └──┘ ┴
702 tendsto_iff_ultrafilter f (𝓝 x) (𝓝 (f x))
id └─────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────────────────┘ ┴ ┴
typ └─────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────────────────────┘ ┴ ┴
703
704 lemma continuous_iff_ultrafilter {f : α → β} :
id ┴ ┴
typ ┴ ┴
705 continuous f ↔ ∀ x g, is_ultrafilter g → g ≤ 𝓝 x → g.map f ≤ 𝓝 (f x) :=
id └────────┘ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴
src └────────┘ ┴ └────────────┘ ┴ ┴ └──┘ ┴ ┴
typ └────────┘ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴
doc └────────┘ └────────────┘ ┴ └──┘ ┴
706 by simp only [continuous_iff_continuous_at, continuous_at_iff_ultrafilter]
id └──────────────────────────┘ └───────────────────────────┘
src └─────────┘└──────────────────────────┘└┘└───────────────────────────┘└─
typ └─────────┘└──────────────────────────┘└┘└───────────────────────────┘└─
doc └─────────┘ └┘ └─
txt └─────────┘ └┘ └─
par └─────────┘ └┘ └─
pid ┴└──┘└┘ └┘ ┴└
st └────────────────────────────────────────────────────────────────────────
707
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
708 /-- A piecewise defined function `if p then f else g` is continuous, if both `f` and `g`
709 are continuous, and they coincide on the frontier (boundary) of the set `{a | p a}`. -/
710 lemma continuous_if {p : α → Prop} {f g : α → β} {h : ∀a, decidable (p a)}
id ┴ ┴ ┴ ┴ └───────┘ ┴ ┴
src └───────┘
typ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴
711 (hp : ∀a∈frontier {a | p a}, f a = g a) (hf : continuous f) (hg : continuous g) :
id ┴ └──────┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴
src └──────┘ ┴ ┴ └────────┘ └────────┘
typ ┴ └──────┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────┘ ┴ └────────┘ ┴
doc └──────┘ └────────┘ └────────┘
712 continuous (λa, @ite (p a) (h a) β (f a) (g a)) :=
id └────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────┘ └─┘
typ └────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────┘
713 continuous_iff_is_closed.mpr $
id └──────────────────────┘└──┘
src └──────────────────────┘└──┘
typ └──────────────────────┘└──┘
714 assume s hs,
id ┴ └┘
typ ┴ └┘
715 have (λa, ite (p a) (f a) (g a)) ⁻¹' s =
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
src └─┘ └─┘ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
doc └─┘
716 (closure {a | p a} ∩ f ⁻¹' s) ∪ (closure {a | ¬ p a} ∩ g ⁻¹' s),
id └─────┘ ┴┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─────┘ ┴┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
src └─────┘ ┴ ┴ └─┘ ┴ └─────┘ ┴ ┴ ┴ └─┘
typ └─────┘ ┴┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─────┘ ┴┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
doc └─────┘ └─┘ └─────┘ └─┘
717 from set.ext $ assume a,
id └─────┘ ┴
src └─────┘
typ └─────┘ ┴
718 classical.by_cases
id └────────────────┘
src └────────────────┘
typ └────────────────┘
719 (assume : a ∈ frontier {a | p a},
id ┴ ┴ └──────┘ ┴┴ ┴ ┴
src ┴ └──────┘ ┴
typ ┴ ┴ └──────┘ ┴┴ ┴ ┴
doc └──────┘
720 have hac : a ∈ closure {a | p a}, from this.left,
id ┴ ┴ └─────┘ ┴┴ ┴ ┴ └──┘└───┘
src ┴ └─────┘ ┴ └───┘
typ ┴ ┴ └─────┘ ┴┴ ┴ ┴ └──┘└───┘
doc └─────┘
721 have hai : a ∈ closure {a | ¬ p a},
id ┴ ┴ └─────┘ ┴┴ ┴ ┴ ┴
src ┴ └─────┘ ┴ ┴
typ ┴ ┴ └─────┘ ┴┴ ┴ ┴ ┴
doc └─────┘
722 from have a ∈ - interior {a | p a}, from this.right, by rwa [←closure_compl] at this,
id ┴ ┴ ┴ └──────┘ ┴┴ ┴ ┴ └──┘└────┘ └───────────┘
src ┴ ┴ └──────┘ ┴ └────┘ └────┘└───────────┘└───────┘
typ ┴ ┴ ┴ └──────┘ ┴┴ ┴ ┴ └──┘└────┘ └────┘└───────────┘└───────┘
doc └──────┘ └────┘ └───────┘
txt └────┘ └───────┘
par └────┘ └───────┘
pid └─┘ ┴└──────┘
st └──────────────────┘┴└──────┘
723 by by_cases p a; simp [h, hp a this, hac, hai, iff_def] {contextual := tt})
id ┴ ┴ ┴ └┘ ┴ └──┘ └─┘ └─┘ └─────┘ └┘
src └───────┘ ┴ └────┘ └┘ ┴ ┴ └┘ └┘ └┘└─────┘└┘ └────────────┘└┘┴
typ └───────┘┴┴┴ └────┘┴└┘└┘┴┴┴└──┘└┘└─┘└┘└─┘└┘└─────┘└┘ └────────────┘└┘┴
doc └───────┘ ┴ └────┘ └┘ ┴ ┴ └┘ └┘ └┘ └┘ └────────────┘ ┴
txt └───────┘ ┴ └────┘ └┘ ┴ ┴ └┘ └┘ └┘ └┘ └────────────┘ ┴
par └───────┘ ┴ └────┘ └┘ ┴ ┴ └┘ └┘ └┘ └┘ └────────────┘ ┴
pid ┴ ┴ ┴┴ └┘ ┴ ┴ └┘ └┘ └┘ ┴┴ └────────────┘ ┴
st └──────────────────────────────────────────────────────────────────────┘
724 (assume hf : a ∈ - frontier {a | p a},
id ┴ ┴ ┴ └──────┘ ┴┴ ┴ ┴
src ┴ ┴ └──────┘ ┴
typ ┴ ┴ ┴ └──────┘ ┴┴ ┴ ┴
doc └──────┘
725 classical.by_cases
id └────────────────┘
src └────────────────┘
typ └────────────────┘
726 (assume : p a,
id ┴ ┴
typ ┴ ┴
727 have hc : a ∈ closure {a | p a}, from subset_closure this,
id ┴ ┴ └─────┘ ┴┴ ┴ ┴ └────────────┘ └──┘
src ┴ └─────┘ ┴ └────────────┘
typ ┴ ┴ └─────┘ ┴┴ ┴ ┴ └────────────┘ └──┘
doc └─────┘
728 have hnc : a ∉ closure {a | ¬ p a},
id ┴ ┴ └─────┘ ┴┴ ┴ ┴ ┴
src ┴ └─────┘ ┴ ┴
typ ┴ ┴ └─────┘ ┴┴ ┴ ┴ ┴
doc └─────┘
729 by show a ∉ closure (- {a | p a}); rw [closure_compl]; simpa [frontier, hc] using hf,
id ┴ ┴ └─────┘ ┴ ┴ ┴ └───────────┘ └──────┘ └┘ └┘
src └───┘ ┴┴┴└─────┘┴ ┴┴┴└──┘ ┴ └┘ └──┘└───────────┘┴ └─────┘└──────┘└┘ └──────┘
typ └───┘┴┴┴┴└─────┘┴ ┴┴┴└──┘┴┴ └┘ └──┘└───────────┘┴ └─────┘└──────┘└┘└┘└──────┘└┘
doc └───┘ ┴ ┴└─────┘┴ ┴ └──┘ ┴ └┘ └──┘ ┴ └─────┘└──────┘└┘ └──────┘
txt └───┘ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ └──┘ ┴ └─────┘ └┘ └──────┘
par └───┘ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ └──┘ ┴ └─────┘ └┘ └──────┘
pid └───┘ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ └┘ ┴ ┴┴ └┘ ┴┴└────┘
st └───────────────────────────────────┘└───────────┘┴└─────────────────────────────┘
730 by simp [this, hc, hnc])
id └──┘ └┘ └─┘
src └────┘ └┘ └┘ ┴
typ └────┘└──┘└┘└┘└┘└─┘┴
doc └────┘ └┘ └┘ ┴
txt └────┘ └┘ └┘ ┴
par └────┘ └┘ └┘ ┴
pid ┴┴ └┘ └┘ ┴
st └───────────────────┘
731 (assume : ¬ p a,
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
732 have hc : a ∈ closure {a | ¬ p a}, from subset_closure this,
id ┴ ┴ └─────┘ ┴┴ ┴ ┴ ┴ └────────────┘ └──┘
src ┴ └─────┘ ┴ ┴ └────────────┘
typ ┴ ┴ └─────┘ ┴┴ ┴ ┴ ┴ └────────────┘ └──┘
doc └─────┘
733 have hnc : a ∉ closure {a | p a},
id ┴ ┴ └─────┘ ┴┴ ┴ ┴
src ┴ └─────┘ ┴
typ ┴ ┴ └─────┘ ┴┴ ┴ ┴
doc └─────┘
734 begin
st └─────
735 have hc : a ∈ closure (- {a | p a}), from hc,
id ┴ └─────┘ ┴ ┴ └┘
src └────────┘ ┴ ┴└─────┘┴ ┴┴└──┘ ┴ └┘ └───┘
typ └────────┘┴┴ ┴└─────┘┴ ┴┴└──┘┴┴ └┘ └───┘└┘
doc └────────┘ ┴ ┴└─────┘┴ ┴ └──┘ ┴ └┘ └───┘
txt └────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ └───┘
par └────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ └───┘
pid └─────┘└─┘ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ └───┘
st ────────────────────────────────────────────────┘└───────┘└─
736 simp [closure_compl] at hc,
id └───────────┘
src └────┘└───────────┘└─────┘
typ └────┘└───────────┘└─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴┴ ┴┴└───┘
st ───────────────────────────────────────┘└─
737 simpa [frontier, hc] using hf
id └──────┘ └┘ └┘
src └─────┘└──────┘└┘ └──────┘ └
typ └─────┘└──────┘└┘└┘└──────┘└┘└
doc └─────┘└──────┘└┘ └──────┘ └
txt └─────┘ └┘ └──────┘ └
par └─────┘ └┘ └──────┘ └
pid ┴┴ └┘ ┴┴└────┘ └
st ────────────────────────────────────────────
738 end,
src ───────────┘
typ ───────────┘
doc ───────────┘
txt ───────────┘
par ───────────┘
pid ───────────┘
st ───────────┘└─┘
739 by simp [this, hc, hnc])),
id └──┘ └┘ └─┘
src └────┘ └┘ └┘ ┴
typ └────┘└──┘└┘└┘└┘└─┘┴
doc └────┘ └┘ └┘ ┴
txt └────┘ └┘ └┘ ┴
par └────┘ └┘ └┘ ┴
pid ┴┴ └┘ └┘ ┴
st └───────────────────┘
740 by rw [this]; exact is_closed_union
id └──┘ └─────────────┘
src └──┘ ┴ └────┘└─────────────┘└
typ └──┘└──┘┴ └────┘└─────────────┘└
doc └──┘ ┴ └────┘ └
txt └──┘ ┴ └────┘ └
par └──┘ ┴ └────┘ └
pid └┘ ┴ ┴ └
st └───────┘┴└───────────────────────
741 (is_closed_inter is_closed_closure $ continuous_iff_is_closed.mp hf s hs)
id └┘
src ─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─
typ ─┘ ┴ ┴ ┴ ┴└┘┴ ┴ └─
doc ─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─
txt ─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─
par ─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─
pid ─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─
st ────────────────────────────────────────────────────────────────────────────
742 (is_closed_inter is_closed_closure $ continuous_iff_is_closed.mp hg s hs)
id └─────────────┘ └───────────────┘ └─────────────────────────┘ └┘ ┴ └┘
src ─┘ └─────────────┘┴└───────────────┘┴ ┴└─────────────────────────┘┴ ┴ ┴ └─
typ ─┘ └─────────────┘┴└───────────────┘┴ ┴└─────────────────────────┘┴└┘┴┴┴└┘└─
doc ─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─
txt ─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─
par ─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─
pid ─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└
st ────────────────────────────────────────────────────────────────────────────
743
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
744
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
745 /- Continuity and partial functions -/
src ───────────────────────────────────────
typ ───────────────────────────────────────
doc ───────────────────────────────────────
txt ───────────────────────────────────────
par ───────────────────────────────────────
pid ───────────────────────────────────────
st ───────────────────────────────────────
746
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
747 /-- Continuity of a partial function -/
748 def pcontinuous (f : α →. β) := ∀ s, is_open s → is_open (f.preimage s)
id ┴ └┘ ┴ ┴ └─────┘ ┴ └─────┘ ┴└───────┘ ┴
src └┘ └─────┘ └─────┘ └───────┘
typ ┴ └┘ ┴ ┴ └─────┘ ┴ └─────┘ ┴└───────┘ ┴
doc └┘ └─────┘ └─────┘
749
750 lemma open_dom_of_pcontinuous {f : α →. β} (h : pcontinuous f) : is_open f.dom :=
id ┴ └┘ ┴ └─────────┘ ┴ └─────┘ ┴└──┘
src └┘ └─────────┘ └─────┘ └──┘
typ ┴ └┘ ┴ └─────────┘ ┴ └─────┘ ┴└──┘
doc └┘ └─────────┘ └─────┘ └──┘
751 by rw [←pfun.preimage_univ]; exact h _ is_open_univ
id └────────────────┘ ┴ └──────────┘
src └───┘└────────────────┘┴ └────┘ └─┘└──────────┘└
typ └───┘└────────────────┘┴ └────┘┴└─┘└──────────┘└
doc └───┘ ┴ └────┘ └─┘ └
txt └───┘ ┴ └────┘ └─┘ └
par └───┘ ┴ └────┘ └─┘ └
pid └─┘ ┴ ┴ └─┘ └
st └──────────────────────┘┴└────────────────────────
752
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
753 lemma pcontinuous_iff' {f : α →. β} :
id ┴ └┘ ┴
src └┘
typ ┴ └┘ ┴
doc └┘
754 pcontinuous f ↔ ∀ {x y} (h : y ∈ f x), ptendsto' f (𝓝 x) (𝓝 y) :=
id └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴
src └─────────┘ ┴ ┴ └───────┘ ┴ ┴
typ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴
doc └─────────┘ ┴ ┴
755 begin
st └─────
756 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
757 { intros h x y h',
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid └───────┘
st ───┘└─────────────┘└─
758 rw [ptendsto'_def],
id └───────────┘
src └──┘└───────────┘┴
typ └──┘└───────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ────────────────────┘└──
759 change ∀ (s : set β), s ∈ (𝓝 y).sets → pfun.preimage f s ∈ (𝓝 x).sets,
id └─┘ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴
src └─────┘ └────┘└─┘┴ ┴ ┴ ┴┴┴ ┴┴ └─────┘ ┴└───────────┘┴ ┴ ┴ ┴ ┴ └────┘
typ └─────┘ └────┘└─┘┴┴┴ ┴ ┴┴┴ ┴┴┴└─────┘ ┴└───────────┘┴┴┴ ┴ ┴ ┴┴└────┘
doc └─────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘
txt └─────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘
par └─────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘
pid ┴ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘┴
st ────────────────────────────────────────────────────────────────────────┘└─
760 rw [nhds_sets, nhds_sets],
id └───────┘ └───────┘
src └──┘└───────┘└┘└───────┘┴
typ └──┘└───────┘└┘└───────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ────────────────┘└─────────┘└──
761 rintros s ⟨t, tsubs, opent, yt⟩,
src └─────────────────────────────┘
typ └─────────────────────────────┘
doc └─────────────────────────────┘
txt └─────────────────────────────┘
par └─────────────────────────────┘
pid └──────────────────────┘
st ──────────────────────────────────┘└─
762 exact ⟨f.preimage t, pfun.preimage_mono _ tsubs, h _ opent, ⟨y, yt, h'⟩⟩
id └────────┘ ┴ └────────────────┘ └───┘ ┴ └───┘ ┴ └┘ └┘
src └────┘ └────────┘┴ └┘└────────────────┘└─┘ └┘ └─┘ └┘ └┘ └┘ └──
typ └────┘ └────────┘┴┴└┘└────────────────┘└─┘└───┘└┘┴└─┘└───┘└┘ ┴└┘└┘└┘└┘└──
doc └────┘ ┴ └┘ └─┘ └┘ └─┘ └┘ └┘ └┘ └──
txt └────┘ ┴ └┘ └─┘ └┘ └─┘ └┘ └┘ └┘ └──
par └────┘ ┴ └┘ └─┘ └┘ └─┘ └┘ └┘ └┘ └──
pid ┴ ┴ └┘ └─┘ └┘ └─┘ └┘ └┘ └┘ └┘└
st ─────────────────────────────────────────────────────────────────────────────
763 },
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└┘└
764 intros hf s os,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └──────┘
st ───────────────┘└─
765 rw is_open_iff_nhds,
id └──────────────┘
src └─┘└──────────────┘
typ └─┘└──────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────────────────┘└─
766 rintros x ⟨y, ys, fxy⟩ t,
src └──────────────────────┘
typ └──────────────────────┘
doc └──────────────────────┘
txt └──────────────────────┘
par └──────────────────────┘
pid └───────────────┘
st ─────────────────────────┘└─
767 rw [mem_principal_sets],
id └────────────────┘
src └──┘└────────────────┘┴
typ └──┘└────────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st ───────────────────────┘└──
768 assume h : f.preimage s ⊆ t,
id └────────┘ ┴ ┴ ┴
src └─────────┘└────────┘┴ ┴┴┴
typ └─────────┘└────────┘┴┴┴┴┴┴
doc └─────────┘ ┴ ┴ ┴
txt └─────────┘ ┴ ┴ ┴
par └─────────┘ ┴ ┴ ┴
pid └─────────┘ ┴ ┴ ┴
st ────────────────────────────┘└─
769 change t ∈ 𝓝 x,
id ┴ ┴
src └─────┘ ┴ ┴ ┴
typ └─────┘┴┴ ┴ ┴┴
doc └─────┘ ┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ──────────────────
770 apply mem_sets_of_superset _ h,
id └──────────────────┘ ┴
src └────┘└──────────────────┘└─┘
typ └────┘└──────────────────┘└─┘┴
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └─┘
st ───────────────────────────────┘└─
771 have h' : ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x,
id ┴ └────────┘ ┴
src └────────┘ └───┘ ┴ ┴└────────┘┴ ┴ ┴ ┴
typ └────────┘ └───┘ ┴┴ ┴└────────┘┴ ┴ ┴ ┴┴
doc └────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
txt └────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
par └────────┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
pid └─────┘└─┘ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────────────┘└─
772 { intros s hs,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ───┘└─────────┘└─
773 have : ptendsto' f (𝓝 x) (𝓝 y) := hf fxy,
id └───────┘ ┴ ┴ ┴ └┘ └─┘
src └─────┘└───────┘┴ ┴ ┴ └┘ ┴ └───┘ ┴
typ └─────┘└───────┘┴┴┴ ┴┴└┘ ┴┴└───┘└┘┴└─┘
doc └─────┘ ┴ ┴ ┴ └┘ ┴ └───┘ ┴
txt └─────┘ ┴ ┴ ┴ └┘ ┴ └───┘ ┴
par └─────┘ ┴ ┴ ┴ └┘ ┴ └───┘ ┴
pid └───┘└┘ ┴ ┴ ┴ └┘ ┴ ┴└──┘ ┴
st ────────────────────────────────────────────┘└─
774 rw ptendsto'_def at this,
id └───────────┘
src └─┘└───────────┘└──────┘
typ └─┘└───────────┘└──────┘
doc └─┘ └──────┘
txt └─┘ └──────┘
par └─┘ └──────┘
pid ┴ └──────┘
st ────────────────────────────┘└─
775 exact this s hs },
id └──┘ ┴ └┘
src └────┘ ┴ ┴ ┴
typ └────┘└──┘┴┴┴└┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ────────────────────┘└┘└
776 show f.preimage s ∈ 𝓝 x,
id └────────┘ ┴ ┴
src └───┘└────────┘┴ ┴ ┴ ┴
typ └───┘└────────┘┴┴┴ ┴ ┴┴
doc └───┘ ┴ ┴ ┴ ┴
txt └───┘ ┴ ┴ ┴ ┴
par └───┘ ┴ ┴ ┴ ┴
pid └───┘ ┴ ┴ ┴ ┴
st ───────────────────────────
777 apply h', rw mem_nhds_sets_iff, exact ⟨s, set.subset.refl _, os, ys⟩
id └───────────────┘ ┴ └─────────────┘ └┘ └┘
src └────┘ └─┘└───────────────┘ └────┘ └┘└─────────────┘└──┘ └┘ └┘
typ └────┘ └─┘└───────────────┘ └────┘ ┴└┘└─────────────┘└──┘└┘└┘└┘└┘
doc └────┘ └─┘ └────┘ └┘ └──┘ └┘ └┘
txt └────┘ └─┘ └────┘ └┘ └──┘ └┘ └┘
par └────┘ └─┘ └────┘ └┘ └──┘ └┘ └┘
pid ┴ ┴ ┴ └┘ └──┘ └┘ ┴┴
st ─────────┘└────────────────────┘└─────────────────────────────────────┘
778 end
st └─┘
779
780 lemma image_closure_subset_closure_image {f : α → β} {s : set α} (h : continuous f) :
id ┴ ┴ └─┘ ┴ └────────┘ ┴
src └─┘ └────────┘
typ ┴ ┴ └─┘ ┴ └────────┘ ┴
doc └────────┘
781 f '' closure s ⊆ closure (f '' s) :=
id ┴ └┘ └─────┘ ┴ ┴ └─────┘ ┴ └┘ ┴
src └┘ └─────┘ ┴ └─────┘ └┘
typ ┴ └┘ └─────┘ ┴ ┴ └─────┘ ┴ └┘ ┴
doc └─────┘ └─────┘
782 have ∀ (a : α), 𝓝 a ⊓ principal s ≠ ⊥ → 𝓝 (f a) ⊓ principal (f '' s) ≠ ⊥,
id ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ └┘ ┴ ┴ ┴
src ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ └───────┘ └┘ ┴ ┴
typ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ └┘ ┴ ┴ ┴
doc ┴ └───────┘ ┴ └───────┘
783 from assume a ha,
id ┴ └┘
typ ┴ └┘
784 have h₁ : ¬ map f (𝓝 a ⊓ principal s) = ⊥,
id ┴ └─┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴
src ┴ └─┘ ┴ ┴ └───────┘ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴
doc └─┘ ┴ └───────┘
785 by rwa[map_eq_bot_iff],
id └────────────┘
src └──┘└────────────┘┴
typ └──┘└────────────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid ┴ ┴
st └─────────────────┘┴
786 have h₂ : map f (𝓝 a ⊓ principal s) ≤ 𝓝 (f a) ⊓ principal (f '' s),
id └─┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ └┘ ┴
src └─┘ ┴ ┴ └───────┘ ┴ ┴ ┴ └───────┘ └┘
typ └─┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ └┘ ┴
doc └─┘ ┴ └───────┘ ┴ └───────┘
787 from le_inf
id └────┘
src └────┘
typ └────┘
788 (le_trans (map_mono inf_le_left) $ by rw [continuous_iff_continuous_at] at h; exact h a)
id └──────┘ └──────┘ └─────────┘ └──────────────────────────┘ ┴ ┴
src └──────┘ └──────┘ └─────────┘ └──┘└──────────────────────────┘└────┘ └────┘ ┴
typ └──────┘ └──────┘ └─────────┘ └──┘└──────────────────────────┘└────┘ └────┘┴┴┴
doc └──┘ └────┘ └────┘ ┴
txt └──┘ └────┘ └────┘ ┴
par └──┘ └────┘ └────┘ ┴
pid └┘ ┴└───┘ ┴ ┴
st └───────────────────────────────┘┴└──────────────┘
789 (le_trans (map_mono inf_le_right) $ by simp; exact subset.refl _),
id └──────┘ └──────┘ └──────────┘
src └──────┘ └──────┘ └──────────┘ └──┘ └────┘ └┘
typ └──────┘ └──────┘ └──────────┘ └──┘ └────┘ └┘
doc └──┘ └────┘ └┘
txt └──┘ └────┘ └┘
par └──┘ └────┘ └┘
pid ┴ └┘
st └────────────────────────┘
790 ne_bot_of_le_ne_bot h₁ h₂,
id └─────────────────┘ └┘ └┘
src └─────────────────┘
typ └─────────────────┘ └┘ └┘
791 by simp [image_subset_iff, closure_eq_nhds]; assumption
id └──────────────┘ └─────────────┘
src └────┘└──────────────┘└┘└─────────────┘┴ └──────────
typ └────┘└──────────────┘└┘└─────────────┘┴ └──────────
doc └────┘└──────────────┘└┘ ┴ └──────────
txt └────┘ └┘ ┴ └──────────
par └────┘ └┘ ┴ └──────────
pid ┴┴ └┘ ┴ └
st └─────────────────────────────────────────────────────
792
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
793 lemma mem_closure {s : set α} {t : set β} {f : α → β} {a : α}
id └─┘ ┴ └─┘ ┴ ┴ ┴ ┴
src └─┘ └─┘
typ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴
794 (hf : continuous f) (ha : a ∈ closure s) (ht : ∀a∈s, f a ∈ t) : f a ∈ closure t :=
id └────────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
src └────────┘ ┴ └─────┘ ┴ ┴ └─────┘
typ └────────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
doc └────────┘ └─────┘ └─────┘
795 subset.trans (image_closure_subset_closure_image hf) (closure_mono $ image_subset_iff.2 ht) $
id └──────────┘ └────────────────────────────────┘ └┘ └──────────┘ └──────────────┘┴ └┘
src └──────────┘ └────────────────────────────────┘ └──────────┘ └──────────────┘┴
typ └──────────┘ └────────────────────────────────┘ └┘ └──────────┘ └──────────────┘┴ └┘
doc └──────────────┘
796 (mem_image_of_mem f ha)
id └──────────────┘ ┴ └┘
src └──────────────┘
typ └──────────────┘ ┴ └┘
797
798 end continuous